Documentation

Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas

Subgroups generated by an element #

Tags #

subgroup, subgroups

source
theorem Subgroup.range_zpowersHom {G : Type u_1} [Group G] (g : G) :
((zpowersHom G) g).range = zpowers g
source
instance Subgroup.instCountableSubtypeMemZpowers {G : Type u_1} [Group G] (a : G) :
Countable ↥(zpowers a)
source
instance AddSubgroup.instCountableSubtypeMemZMultiples {G : Type u_1} [AddGroup G] (a : G) :
Countable ↥(zmultiples a)
source
theorem Subgroup.finsetSup_zpowers {G : Type u_1} [Group G] (s : Finset G) :
s.sup zpowers = closure ↑s
source
theorem AddSubgroup.finsetSup_zmultiples {G : Type u_1} [AddGroup G] (s : Finset G) :
s.sup zmultiples = closure ↑s
source
@[simp]
theorem AddSubgroup.range_zmultiplesHom {A : Type u_2} [AddGroup A] (a : A) :
((zmultiplesHom A) a).range = zmultiples a
source
noncomputable def AddSubgroup.zmultiplesEquivInt {A : Type u_2} [AddGroup A] [IsAddTorsionFree A] {a : A} (ha : a ≠ 0) :
↥(zmultiples a) ≃+ ℤ

The subgroup generated by a nonzero element a of a torsion-free additive group is isomorphic to ℤ, sending n • a to n.

Equations
Instances For
    source
    @[simp]
    theorem AddSubgroup.coe_zmultiplesEquivInt_symm_apply {A : Type u_2} [AddGroup A] [IsAddTorsionFree A] {a : A} (ha : a ≠ 0) (n : ℤ) :
    ↑((zmultiplesEquivInt ha).symm n) = n • a
    source
    @[simp]
    theorem AddSubgroup.zmultiplesEquivInt_apply_zsmul {A : Type u_2} [AddGroup A] [IsAddTorsionFree A] {a : A} (ha : a ≠ 0) (n : ℤ) :
    (zmultiplesEquivInt ha) ⟨n • a, ⋯⟩ = n
    source
    @[simp]
    theorem AddSubgroup.intCast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ℤ) :
    ↑k * r ∈ zmultiples r
    source
    @[simp]
    theorem AddSubgroup.intCast_mem_zmultiples_one {R : Type u_4} [Ring R] (k : ℤ) :
    ↑k ∈ zmultiples 1
    source
    @[simp]
    theorem Int.range_castAddHom {A : Type u_4} [AddGroupWithOne A] :
    (castAddHom A).range = AddSubgroup.zmultiples 1
    source
    theorem Int.range_nsmulAddMonoidHom (n : ℕ) :
    (nsmulAddMonoidHom n).range = AddSubgroup.zmultiples ↑n
    source
    theorem Int.closure_eq_zmultiples (a b : ℤ) :
    AddSubgroup.closure {a, b} = AddSubgroup.zmultiples ↑(a.gcd b)
    source
    theorem Int.closure_eq_zmultiples_finsetGcd (s : Finset ℤ) :
    AddSubgroup.closure ↑s = AddSubgroup.zmultiples (s.gcd id)
    source
    theorem Int.zmultiples_sup (a b : ℤ) :
    AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples b = AddSubgroup.zmultiples ↑(a.gcd b)
    source
    theorem Int.finsetSup_zmultiples (s : Finset ℤ) :
    s.sup AddSubgroup.zmultiples = AddSubgroup.zmultiples (s.gcd id)
    source
    theorem Int.zmultiples_inf (a b : ℤ) :
    AddSubgroup.zmultiples a ⊓ AddSubgroup.zmultiples b = AddSubgroup.zmultiples ↑(a.lcm b)
    source
    theorem Int.finsetInf_zmultiples (s : Finset ℤ) :
    s.inf AddSubgroup.zmultiples = AddSubgroup.zmultiples (s.lcm id)