mathlib3 documentation

group_theory.subgroup.zpowers

Subgroups generated by an element #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Tags #

subgroup, subgroups

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

The subgroup generated by an element.

Equations
Instances for subgroup.zpowers
Instances for subgroup.zpowers
@[simp]
theorem subgroup.mem_zpowers {G : Type u_1} [group G] (g : G) :
@[norm_cast]
theorem subgroup.coe_zpowers {G : Type u_1} [group G] (g : G) :
(subgroup.zpowers g) = set.range (λ (n : ), g ^ n)
@[simp]
theorem subgroup.range_zpowers_hom {G : Type u_1} [group G] (g : G) :
theorem subgroup.mem_zpowers_iff {G : Type u_1} [group G] {g h : G} :
h subgroup.zpowers g (k : ), g ^ k = h
@[simp]
theorem subgroup.zpow_mem_zpowers {G : Type u_1} [group G] (g : G) (k : ) :
@[simp]
theorem subgroup.npow_mem_zpowers {G : Type u_1} [group G] (g : G) (k : ) :
@[simp]
theorem subgroup.forall_zpowers {G : Type u_1} [group G] {x : G} {p : (subgroup.zpowers x) Prop} :
( (g : (subgroup.zpowers x)), p g) (m : ), p x ^ m, _⟩
@[simp]
theorem subgroup.exists_zpowers {G : Type u_1} [group G] {x : G} {p : (subgroup.zpowers x) Prop} :
( (g : (subgroup.zpowers x)), p g) (m : ), p x ^ m, _⟩
theorem subgroup.forall_mem_zpowers {G : Type u_1} [group G] {x : G} {p : G Prop} :
( (g : G), g subgroup.zpowers x p g) (m : ), p (x ^ m)
theorem subgroup.exists_mem_zpowers {G : Type u_1} [group G] {x : G} {p : G Prop} :
( (g : G) (H : g subgroup.zpowers x), p g) (m : ), p (x ^ m)
@[protected, instance]
def add_subgroup.zmultiples {A : Type u_2} [add_group A] (a : A) :

The subgroup generated by an element.

Equations
Instances for add_subgroup.zmultiples
Instances for add_subgroup.zmultiples
@[simp]
@[norm_cast]
theorem add_subgroup.coe_zmultiples {G : Type u_1} [add_group G] (g : G) :
theorem add_subgroup.mem_zmultiples_iff {G : Type u_1} [add_group G] {g h : G} :
@[simp]
theorem add_subgroup.zsmul_mem_zmultiples {G : Type u_1} [add_group G] (g : G) (k : ) :
@[simp]
theorem add_subgroup.nsmul_mem_zmultiples {G : Type u_1} [add_group G] (g : G) (k : ) :
@[simp]
theorem add_subgroup.forall_zmultiples {G : Type u_1} [add_group G] {x : G} {p : (add_subgroup.zmultiples x) Prop} :
( (g : (add_subgroup.zmultiples x)), p g) (m : ), p m x, _⟩
theorem add_subgroup.forall_mem_zmultiples {G : Type u_1} [add_group G] {x : G} {p : G Prop} :
( (g : G), g add_subgroup.zmultiples x p g) (m : ), p (m x)
@[simp]
theorem add_subgroup.exists_zmultiples {G : Type u_1} [add_group G] {x : G} {p : (add_subgroup.zmultiples x) Prop} :
( (g : (add_subgroup.zmultiples x)), p g) (m : ), p m x, _⟩
theorem add_subgroup.exists_mem_zmultiples {G : Type u_1} [add_group G] {x : G} {p : G Prop} :
( (g : G) (H : g add_subgroup.zmultiples x), p g) (m : ), p (m x)
@[protected, instance]
@[simp]
@[simp]
@[simp]
theorem monoid_hom.map_zpowers {G : Type u_1} [group G] {N : Type u_3} [group N] (f : G →* N) (x : G) :
@[protected, instance]
@[protected, instance]
@[simp]
theorem subgroup.zpowers_le {G : Type u_1} [group G] {g : G} {H : subgroup G} :
@[simp]
theorem add_subgroup.zmultiples_le {G : Type u_1} [add_group G] {g : G} {H : add_subgroup G} :
theorem subgroup.zpowers_le_of_mem {G : Type u_1} [group G] {g : G} {H : subgroup G} :

Alias of the reverse direction of subgroup.zpowers_le.

Alias of the reverse direction of add_subgroup.zmultiples_le.

@[simp]
@[simp]
theorem subgroup.zpowers_eq_bot {G : Type u_1} [group G] {g : G} :
theorem subgroup.zpowers_ne_bot {G : Type u_1} [group G] {g : G} :
@[simp]
theorem subgroup.centralizer_closure {G : Type u_1} [group G] (S : set G) :
theorem subgroup.center_eq_infi {G : Type u_1} [group G] (S : set G) (hS : subgroup.closure S = ) :