Subgroups generated by an element

Tags

subgroup, subgroups

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 Int.range_nsmulAddMonoidHom (n : ℕ) : (nsmulAddMonoidHom n).range = AddSubgroup.zmultiples ↑n