# Subgroups generated by an element #

## Tags #

subgroup, subgroups

def Subgroup.zpowers {G : Type u_1} [] (g : G) :

The subgroup generated by an element.

Equations
Instances For
@[simp]
theorem Subgroup.mem_zpowers {G : Type u_1} [] (g : G) :
theorem Subgroup.coe_zpowers {G : Type u_1} [] (g : G) :
() = Set.range fun (x : ) => g ^ x
noncomputable instance Subgroup.decidableMemZPowers {G : Type u_1} [] {a : G} :
DecidablePred fun (x : G) =>
Equations
theorem Subgroup.zpowers_eq_closure {G : Type u_1} [] (g : G) :
@[simp]
theorem Subgroup.range_zpowersHom {G : Type u_1} [] (g : G) :
(() g).range =
theorem Subgroup.mem_zpowers_iff {G : Type u_1} [] {g : G} {h : G} :
∃ (k : ), g ^ k = h
@[simp]
theorem Subgroup.zpow_mem_zpowers {G : Type u_1} [] (g : G) (k : ) :
g ^ k
@[simp]
theorem Subgroup.npow_mem_zpowers {G : Type u_1} [] (g : G) (k : ) :
g ^ k
@[simp]
theorem Subgroup.forall_zpowers {G : Type u_1} [] {x : G} {p : ()Prop} :
(∀ (g : ()), p g) ∀ (m : ), p x ^ m,
@[simp]
theorem Subgroup.exists_zpowers {G : Type u_1} [] {x : G} {p : ()Prop} :
(∃ (g : ()), p g) ∃ (m : ), p x ^ m,
theorem Subgroup.forall_mem_zpowers {G : Type u_1} [] {x : G} {p : GProp} :
(g, p g) ∀ (m : ), p (x ^ m)
theorem Subgroup.exists_mem_zpowers {G : Type u_1} [] {x : G} {p : GProp} :
(g, p g) ∃ (m : ), p (x ^ m)
instance Subgroup.instCountableSubtypeMemZpowers {G : Type u_1} [] (a : G) :
Equations
• =
def AddSubgroup.zmultiples {A : Type u_2} [] (a : A) :

The subgroup generated by an element.

Equations
Instances For
@[simp]
theorem AddSubgroup.range_zmultiplesHom {A : Type u_2} [] (a : A) :
(() a).range =
@[simp]
theorem AddSubgroup.mem_zmultiples {G : Type u_1} [] (g : G) :
theorem AddSubgroup.coe_zmultiples {G : Type u_1} [] (g : G) :
= Set.range fun (x : ) => x g
noncomputable instance AddSubgroup.decidableMemZMultiples {G : Type u_1} [] {a : G} :
DecidablePred fun (x : G) =>
Equations
theorem AddSubgroup.zmultiples_eq_closure {G : Type u_1} [] (g : G) :
theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [] {g : G} {h : G} :
∃ (k : ), k g = h
@[simp]
theorem AddSubgroup.zsmul_mem_zmultiples {G : Type u_1} [] (g : G) (k : ) :
k g
@[simp]
theorem AddSubgroup.nsmul_mem_zmultiples {G : Type u_1} [] (g : G) (k : ) :
k g
@[simp]
theorem AddSubgroup.forall_zmultiples {G : Type u_1} [] {x : G} {p : } :
(∀ (g : ), p g) ∀ (m : ), p m x,
theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [] {x : G} {p : GProp} :
(g, p g) ∀ (m : ), p (m x)
@[simp]
theorem AddSubgroup.exists_zmultiples {G : Type u_1} [] {x : G} {p : } :
(∃ (g : ), p g) ∃ (m : ), p m x,
theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [] {x : G} {p : GProp} :
(g, p g) ∃ (m : ), p (m x)
instance AddSubgroup.instCountableSubtypeMemZmultiples {A : Type u_2} [] (a : A) :
Equations
• =
@[simp]
theorem AddSubgroup.intCast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ) :
k * r
theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ) :
k * r

Alias of AddSubgroup.intCast_mul_mem_zmultiples.

@[simp]
theorem AddSubgroup.intCast_mem_zmultiples_one {R : Type u_4} [Ring R] (k : ) :

Alias of AddSubgroup.intCast_mem_zmultiples_one.

@[simp]
theorem Int.range_castAddHom {A : Type u_4} [] :
().range =
@[simp]
theorem AddMonoidHom.map_zmultiples {G : Type u_1} [] {N : Type u_3} [] (f : G →+ N) (x : G) :
@[simp]
theorem MonoidHom.map_zpowers {G : Type u_1} [] {N : Type u_3} [] (f : G →* N) (x : G) :
theorem Int.mem_zmultiples_iff {a : } {b : } :
a b
@[simp]
theorem ofMul_image_zpowers_eq_zmultiples_ofMul {G : Type u_1} [] {x : G} :
abbrev AddSubgroup.zmultiples_isCommutative.match_1 {G : Type u_1} [] (g : G) (motive : ) :
∀ (x : ), (∀ (val : G) (w : ) (h₂ : (fun (x : ) => x g) w = val), motive val, )motive x
Equations
• =
Instances For
instance AddSubgroup.zmultiples_isCommutative {G : Type u_1} [] (g : G) :
.IsCommutative
Equations
• =
instance Subgroup.zpowers_isCommutative {G : Type u_1} [] (g : G) :
().IsCommutative
Equations
• =
@[simp]
theorem AddSubgroup.zmultiples_le {G : Type u_1} [] {g : G} {H : } :
g H
@[simp]
theorem Subgroup.zpowers_le {G : Type u_1} [] {g : G} {H : } :
g H
theorem Subgroup.zpowers_le_of_mem {G : Type u_1} [] {g : G} {H : } :
g H

Alias of the reverse direction of Subgroup.zpowers_le.

theorem AddSubgroup.zmultiples_le_of_mem {G : Type u_1} [] {g : G} {H : } :
g H

Alias of the reverse direction of AddSubgroup.zmultiples_le.

@[simp]
theorem AddSubgroup.zmultiples_eq_bot {G : Type u_1} [] {g : G} :
g = 0
@[simp]
theorem Subgroup.zpowers_eq_bot {G : Type u_1} [] {g : G} :
g = 1
theorem AddSubgroup.zmultiples_ne_bot {G : Type u_1} [] {g : G} :
g 0
theorem Subgroup.zpowers_ne_bot {G : Type u_1} [] {g : G} :
g 1
@[simp]
@[simp]
theorem Subgroup.zpowers_one_eq_bot {G : Type u_1} [] :
theorem AddSubgroup.centralizer_closure {G : Type u_1} [] (S : Set G) :
theorem Subgroup.centralizer_closure {G : Type u_1} [] (S : Set G) :
= gS,
theorem AddSubgroup.center_eq_iInf {G : Type u_1} [] (S : Set G) (hS : ) :
=
theorem Subgroup.center_eq_iInf {G : Type u_1} [] (S : Set G) (hS : ) :
= gS,
theorem AddSubgroup.center_eq_infi' {G : Type u_1} [] (S : Set G) (hS : ) :
= ⨅ (g : S),
theorem Subgroup.center_eq_infi' {G : Type u_1} [] (S : Set G) (hS : ) :
= ⨅ (g : S),