Documentation

Mathlib.Algebra.Group.Subgroup.ZPowers.Basic

Subgroups generated by an element #

Tags #

subgroup, subgroups

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

The subgroup generated by an element.

Equations
Instances For
def AddSubgroup.zmultiples {G : Type u_1} [AddGroup G] (g : G) :

The additive subgroup generated by an element.

Equations
Instances For
@[simp]
theorem Subgroup.mem_zpowers {G : Type u_1} [Group G] (g : G) :
@[simp]
theorem AddSubgroup.mem_zmultiples {G : Type u_1} [AddGroup G] (g : G) :
theorem Subgroup.coe_zpowers {G : Type u_1} [Group G] (g : G) :
(zpowers g) = Set.range fun (x : ) => g ^ x
theorem AddSubgroup.coe_zmultiples {G : Type u_1} [AddGroup G] (g : G) :
(zmultiples g) = Set.range fun (x : ) => x g
noncomputable instance Subgroup.decidableMemZPowers {G : Type u_1} [Group G] {a : G} :
DecidablePred fun (x : G) => x zpowers a
Equations
theorem Subgroup.zpowers_eq_closure {G : Type u_1} [Group G] (g : G) :
theorem Subgroup.mem_zpowers_iff {G : Type u_1} [Group G] {g h : G} :
h zpowers g ∃ (k : ), g ^ k = h
theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [AddGroup G] {g h : G} :
h zmultiples g ∃ (k : ), k g = h
@[simp]
theorem Subgroup.zpow_mem_zpowers {G : Type u_1} [Group G] (g : G) (k : ) :
g ^ k zpowers g
@[simp]
theorem AddSubgroup.zsmul_mem_zmultiples {G : Type u_1} [AddGroup G] (g : G) (k : ) :
@[simp]
theorem Subgroup.npow_mem_zpowers {G : Type u_1} [Group G] (g : G) (k : ) :
g ^ k zpowers g
@[simp]
theorem AddSubgroup.nsmul_mem_zmultiples {G : Type u_1} [AddGroup G] (g : G) (k : ) :
@[simp]
theorem Subgroup.forall_zpowers {G : Type u_1} [Group G] {x : G} {p : (zpowers x)Prop} :
(∀ (g : (zpowers x)), p g) ∀ (m : ), p x ^ m,
@[simp]
theorem AddSubgroup.forall_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : (zmultiples x)Prop} :
(∀ (g : (zmultiples x)), p g) ∀ (m : ), p m x,
@[simp]
theorem Subgroup.exists_zpowers {G : Type u_1} [Group G] {x : G} {p : (zpowers x)Prop} :
(∃ (g : (zpowers x)), p g) ∃ (m : ), p x ^ m,
@[simp]
theorem AddSubgroup.exists_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : (zmultiples x)Prop} :
(∃ (g : (zmultiples x)), p g) ∃ (m : ), p m x,
theorem Subgroup.forall_mem_zpowers {G : Type u_1} [Group G] {x : G} {p : GProp} :
(∀ gzpowers x, p g) ∀ (m : ), p (x ^ m)
theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : GProp} :
(∀ gzmultiples x, p g) ∀ (m : ), p (m x)
theorem Subgroup.exists_mem_zpowers {G : Type u_1} [Group G] {x : G} {p : GProp} :
(∃ gzpowers x, p g) ∃ (m : ), p (x ^ m)
theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : GProp} :
(∃ gzmultiples x, p g) ∃ (m : ), p (m x)
@[simp]
theorem MonoidHom.map_zpowers {G : Type u_1} [Group G] {N : Type u_3} [Group N] (f : G →* N) (x : G) :
@[simp]
@[simp]
theorem Subgroup.zpowers_le {G : Type u_1} [Group G] {g : G} {H : Subgroup G} :
zpowers g H g H
@[simp]
theorem AddSubgroup.zmultiples_le {G : Type u_1} [AddGroup G] {g : G} {H : AddSubgroup G} :
theorem Subgroup.zpowers_le_of_mem {G : Type u_1} [Group G] {g : G} {H : Subgroup G} :
g Hzpowers g H

Alias of the reverse direction of Subgroup.zpowers_le.

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

Alias of the reverse direction of AddSubgroup.zmultiples_le.

@[simp]
theorem Subgroup.zpowers_eq_bot {G : Type u_1} [Group G] {g : G} :
zpowers g = g = 1
@[simp]
theorem AddSubgroup.zmultiples_eq_bot {G : Type u_1} [AddGroup G] {g : G} :
theorem Subgroup.zpowers_ne_bot {G : Type u_1} [Group G] {g : G} :
@[simp]
@[simp]
theorem Subgroup.zpowers_inv {G : Type u_1} [Group G] {g : G} :
@[simp]
theorem AddSubgroup.zmultiples_neg {G : Type u_1} [AddGroup G] {g : G} :