# Documentation

Mathlib.GroupTheory.Subgroup.Zpowers

# Subgroups generated by an element #

## Tags #

subgroup, subgroups

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

The subgroup generated by an element.

Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem Subgroup.mem_zpowers {G : Type u_1} [inst : ] (g : G) :
theorem Subgroup.zpowers_eq_closure {G : Type u_1} [inst : ] (g : G) :
@[simp]
theorem Subgroup.range_zpowersHom {G : Type u_1} [inst : ] (g : G) :
MonoidHom.range (↑() g) =
theorem Subgroup.zpowers_subset {G : Type u_1} [inst : ] {a : G} {K : } (h : a K) :
theorem Subgroup.mem_zpowers_iff {G : Type u_1} [inst : ] {g : G} {h : G} :
k, g ^ k = h
@[simp]
theorem Subgroup.zpow_mem_zpowers {G : Type u_1} [inst : ] (g : G) (k : ) :
g ^ k
@[simp]
theorem Subgroup.npow_mem_zpowers {G : Type u_1} [inst : ] (g : G) (k : ) :
g ^ k
@[simp]
theorem Subgroup.forall_zpowers {G : Type u_1} [inst : ] {x : G} {p : { x // }Prop} :
((g : { x // }) → p g) (m : ) → p { val := x ^ m, property := (_ : y, (fun x x_1 => x ^ x_1) x y = x ^ m) }
@[simp]
theorem Subgroup.exists_zpowers {G : Type u_1} [inst : ] {x : G} {p : { x // }Prop} :
(g, p g) m, p { val := x ^ m, property := (_ : y, (fun x x_1 => x ^ x_1) x y = x ^ m) }
theorem Subgroup.forall_mem_zpowers {G : Type u_1} [inst : ] {x : G} {p : GProp} :
((g : G) → p g) (m : ) → p (x ^ m)
theorem Subgroup.exists_mem_zpowers {G : Type u_1} [inst : ] {x : G} {p : GProp} :
(g, p g) m, p (x ^ m)
def AddSubgroup.zmultiples {A : Type u_1} [inst : ] (a : A) :

The subgroup generated by an element.

Equations
@[simp]
theorem AddSubgroup.range_zmultiplesHom {A : Type u_1} [inst : ] (a : A) :
@[simp]
theorem AddSubgroup.mem_zmultiples {G : Type u_1} [inst : ] (g : G) :
theorem AddSubgroup.zmultiples_eq_closure {G : Type u_1} [inst : ] (g : G) :
abbrev AddSubgroup.zmultiples_subset.match_1 {G : Type u_1} [inst : ] {a : G} (motive : (x : G) → ) :
(x : G) → (hx : ) → ((i : ) → motive ((fun x x_1 => x_1 x) a i) (_ : y, (fun x x_1 => x_1 x) a y = (fun x x_1 => x_1 x) a i)) → motive x hx
Equations
• One or more equations did not get rendered due to their size.
theorem AddSubgroup.zmultiples_subset {G : Type u_1} [inst : ] {a : G} {K : } (h : a K) :
theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [inst : ] {g : G} {h : G} :
k, k g = h
@[simp]
theorem AddSubgroup.zsmul_mem_zmultiples {G : Type u_1} [inst : ] (g : G) (k : ) :
k g
@[simp]
theorem AddSubgroup.nsmul_mem_zmultiples {G : Type u_1} [inst : ] (g : G) (k : ) :
k g
@[simp]
theorem AddSubgroup.forall_zmultiples {G : Type u_1} [inst : ] {x : G} {p : { x // }Prop} :
((g : { x // }) → p g) (m : ) → p { val := m x, property := (_ : y, (fun x x_1 => x_1 x) x y = m x) }
theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [inst : ] {x : G} {p : GProp} :
((g : G) → p g) (m : ) → p (m x)
@[simp]
theorem AddSubgroup.exists_zmultiples {G : Type u_1} [inst : ] {x : G} {p : { x // }Prop} :
(g, p g) m, p { val := m x, property := (_ : y, (fun x x_1 => x_1 x) x y = m x) }
theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [inst : ] {x : G} {p : GProp} :
(g, p g) m, p (m x)
@[simp]
theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_1} [inst : Ring R] (r : R) (k : ) :
k * r
@[simp]
theorem AddSubgroup.int_cast_mem_zmultiples_one {R : Type u_1} [inst : Ring R] (k : ) :
@[simp]
theorem AddMonoidHom.map_zmultiples {G : Type u_1} [inst : ] {N : Type u_2} [inst : ] (f : G →+ N) (x : G) :
@[simp]
theorem MonoidHom.map_zpowers {G : Type u_1} [inst : ] {N : Type u_2} [inst : ] (f : G →* N) (x : G) :
theorem Int.mem_zmultiples_iff {a : } {b : } :
a b
theorem ofMul_image_zpowers_eq_zmultiples_ofMul {G : Type u_1} [inst : ] {x : G} :
theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {A : Type u_1} [inst : ] {x : A} :
def AddSubgroup.zmultiples_isCommutative.proof_1 {G : Type u_1} [inst : ] (g : G) :
Equations
abbrev AddSubgroup.zmultiples_isCommutative.match_1 {G : Type u_1} [inst : ] (g : G) (motive : { x // }Prop) :
(x : { x // }) → ((val : G) → (w : ) → (h₂ : (fun x x_1 => x_1 x) g w = val) → motive { val := val, property := (_ : y, (fun x x_1 => x_1 x) g y = val) }) → motive x
Equations
instance AddSubgroup.zmultiples_isCommutative {G : Type u_1} [inst : ] (g : G) :
Equations
instance Subgroup.zpowers_isCommutative {G : Type u_1} [inst : ] (g : G) :
Equations
@[simp]
theorem AddSubgroup.zmultiples_le {G : Type u_1} [inst : ] {g : G} {H : } :
g H
@[simp]
theorem Subgroup.zpowers_le {G : Type u_1} [inst : ] {g : G} {H : } :
g H
@[simp]
theorem AddSubgroup.zmultiples_eq_bot {G : Type u_1} [inst : ] {g : G} :
g = 0
@[simp]
theorem Subgroup.zpowers_eq_bot {G : Type u_1} [inst : ] {g : G} :
g = 1
@[simp]
theorem AddSubgroup.zmultiples_zero_eq_bot {G : Type u_1} [inst : ] :
@[simp]
theorem Subgroup.zpowers_one_eq_bot {G : Type u_1} [inst : ] :
theorem AddSubgroup.centralizer_closure {G : Type u_1} [inst : ] (S : Set G) :
theorem Subgroup.centralizer_closure {G : Type u_1} [inst : ] (S : Set G) :
= g,
theorem AddSubgroup.center_eq_infᵢ {G : Type u_1} [inst : ] (S : Set G) (hS : ) :
= g,
theorem Subgroup.center_eq_infᵢ {G : Type u_1} [inst : ] (S : Set G) (hS : ) :
= g,
theorem AddSubgroup.center_eq_infi' {G : Type u_1} [inst : ] (S : Set G) (hS : ) :
theorem Subgroup.center_eq_infi' {G : Type u_1} [inst : ] (S : Set G) (hS : ) :
= g,