Subgroups generated by an element

Tags

subgroup, subgroups

@[simp]

theorem Subgroup.range_zpowersHom {G : Type u_1} [Group G] (g : G) : ((zpowersHom G) g).range = Subgroup.zpowers g

instance Subgroup.instCountableSubtypeMemZpowers {G : Type u_1} [Group G] (a : G) : Countable ↥(Subgroup.zpowers a)

instance AddSubgroup.instCountableSubtypeMemZmultiples {G : Type u_1} [AddGroup G] (a : G) : Countable ↥(AddSubgroup.zmultiples a)

@[simp]

theorem AddSubgroup.range_zmultiplesHom {A : Type u_2} [AddGroup A] (a : A) : ((zmultiplesHom A) a).range = AddSubgroup.zmultiples a

@[simp]

theorem AddSubgroup.intCast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ℤ) : ↑k * r ∈ AddSubgroup.zmultiples r

@[deprecated AddSubgroup.intCast_mul_mem_zmultiples]

theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ℤ) : ↑k * r ∈ AddSubgroup.zmultiples r

Alias of AddSubgroup.intCast_mul_mem_zmultiples.

@[simp]

theorem AddSubgroup.intCast_mem_zmultiples_one {R : Type u_4} [Ring R] (k : ℤ) : ↑k ∈ AddSubgroup.zmultiples 1

@[deprecated AddSubgroup.intCast_mem_zmultiples_one]

theorem AddSubgroup.int_cast_mem_zmultiples_one {R : Type u_4} [Ring R] (k : ℤ) : ↑k ∈ AddSubgroup.zmultiples 1

Alias of AddSubgroup.intCast_mem_zmultiples_one.

@[simp]

theorem Int.range_castAddHom {A : Type u_4} [AddGroupWithOne A] : (Int.castAddHom A).range = AddSubgroup.zmultiples 1

theorem Subgroup.centralizer_closure {G : Type u_1} [Group G] (S : Set G) : Subgroup.centralizer ↑(Subgroup.closure S) = ⨅ g ∈ S, Subgroup.centralizer ↑(Subgroup.zpowers g)

theorem AddSubgroup.centralizer_closure {G : Type u_1} [AddGroup G] (S : Set G) : AddSubgroup.centralizer ↑(AddSubgroup.closure S) = ⨅ g ∈ S, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples g)

theorem Subgroup.center_eq_iInf {G : Type u_1} [Group G] (S : Set G) (hS : Subgroup.closure S = ⊤) : Subgroup.center G = ⨅ g ∈ S, Subgroup.centralizer ↑(Subgroup.zpowers g)

theorem AddSubgroup.center_eq_iInf {G : Type u_1} [AddGroup G] (S : Set G) (hS : AddSubgroup.closure S = ⊤) : AddSubgroup.center G = ⨅ g ∈ S, AddSubgroup.centralizer ↑(AddSubgroup.zmultiples g)

theorem Subgroup.center_eq_infi' {G : Type u_1} [Group G] (S : Set G) (hS : Subgroup.closure S = ⊤) : Subgroup.center G = ⨅ (g : ↑S), Subgroup.centralizer ↑(Subgroup.zpowers ↑g)

theorem AddSubgroup.center_eq_infi' {G : Type u_1} [AddGroup G] (S : Set G) (hS : AddSubgroup.closure S = ⊤) : AddSubgroup.center G = ⨅ (g : ↑S), AddSubgroup.centralizer ↑(AddSubgroup.zmultiples ↑g)