ℤ-multiples of a non-torsion element

For an element p of an additive group that is not of finite additive order, the subgroup zmultiples p of its ℤ-multiples is infinite cyclic: n ↦ n • p is an isomorphism ℤ ≃+ zmultiples p. This applies Mathlib's intEquivOfZMultiplesEqTop to the subgroup zmultiples p itself.

Main declarations

• TauCeti.intEquivZMultiples: the isomorphism ℤ ≃+ zmultiples p for a non-torsion p.

noncomputable def TauCeti.intEquivZMultiples {G : Type u_1} [AddGroup G] {p : G} (hp : ¬IsOfFinAddOrder p) : ℤ ≃+ ↥(AddSubgroup.zmultiples p)

For an element p of infinite additive order, the subgroup zmultiples p is infinite cyclic, identified with ℤ by n ↦ n • p.

Equations

• TauCeti.intEquivZMultiples hp = intEquivOfZMultiplesEqTop ⟨p, ⋯⟩ ⋯

@[simp]

theorem TauCeti.intEquivZMultiples_apply {G : Type u_1} [AddGroup G] {p : G} (hp : ¬IsOfFinAddOrder p) (n : ℤ) : ↑((intEquivZMultiples hp) n) = n • p

@[simp]

theorem TauCeti.intEquivZMultiples_symm_mk_zsmul {G : Type u_1} [AddGroup G] {p : G} (hp : ¬IsOfFinAddOrder p) (n : ℤ) : (intEquivZMultiples hp).symm ⟨n • p, ⋯⟩ = n

theorem TauCeti.intEquivZMultiples_symm_zsmul {G : Type u_1} [AddGroup G] {p : G} (hp : ¬IsOfFinAddOrder p) (a : ↥(AddSubgroup.zmultiples p)) : (intEquivZMultiples hp).symm a • p = ↑a