# 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
@[simp]
theorem AddSubgroup.range_zmultiplesHom {A : Type u_2} [AddGroup A] (a : A) :
((zmultiplesHom A) a).range = zmultiples a
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 Subgroup.centralizer_closure {G : Type u_1} [Group G] (S : Set G) :
centralizer ↑(closure S) = ⨅ g ∈ S, centralizer ↑(zpowers g)
source
theorem AddSubgroup.centralizer_closure {G : Type u_1} [AddGroup G] (S : Set G) :
centralizer ↑(closure S) = ⨅ g ∈ S, centralizer ↑(zmultiples g)
source
theorem Subgroup.center_eq_iInf {G : Type u_1} [Group G] (S : Set G) (hS : closure S = ⊤) :
center G = ⨅ g ∈ S, centralizer ↑(zpowers g)
source
theorem AddSubgroup.center_eq_iInf {G : Type u_1} [AddGroup G] (S : Set G) (hS : closure S = ⊤) :
center G = ⨅ g ∈ S, centralizer ↑(zmultiples g)
source
theorem Subgroup.center_eq_infi' {G : Type u_1} [Group G] (S : Set G) (hS : closure S = ⊤) :
center G = ⨅ (g : ↑S), centralizer ↑(zpowers ↑g)
source
theorem AddSubgroup.center_eq_infi' {G : Type u_1} [AddGroup G] (S : Set G) (hS : closure S = ⊤) :
center G = ⨅ (g : ↑S), centralizer ↑(zmultiples ↑g)