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 = zpowers g

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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