Documentation

Mathlib.GroupTheory.Subgroup.ZPowers

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
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Subgroup.mem_zpowers {G : Type u_1} [Group G] (g : G) :
    theorem Subgroup.coe_zpowers {G : Type u_1} [Group G] (g : G) :
    ↑(Subgroup.zpowers g) = Set.range fun x => g ^ x
    @[simp]
    theorem Subgroup.mem_zpowers_iff {G : Type u_1} [Group G] {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 : { x // x Subgroup.zpowers x }Prop} :
    ((g : { x // x Subgroup.zpowers 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} [Group G] {x : G} {p : { x // x Subgroup.zpowers 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} [Group G] {x : G} {p : GProp} :
    ((g : G) → g Subgroup.zpowers xp g) (m : ) → p (x ^ m)
    theorem Subgroup.exists_mem_zpowers {G : Type u_1} [Group G] {x : G} {p : GProp} :
    (g, g Subgroup.zpowers x p g) m, p (x ^ m)
    def AddSubgroup.zmultiples {A : Type u_2} [AddGroup A] (a : A) :

    The subgroup generated by an element.

    Equations
    Instances For
      @[simp]
      theorem AddSubgroup.coe_zmultiples {G : Type u_1} [AddGroup G] (g : G) :
      theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [AddGroup G] {g : G} {h : G} :
      @[simp]
      @[simp]
      @[simp]
      theorem AddSubgroup.forall_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : { x // x AddSubgroup.zmultiples x }Prop} :
      ((g : { x // x AddSubgroup.zmultiples 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} [AddGroup G] {x : G} {p : GProp} :
      ((g : G) → g AddSubgroup.zmultiples xp g) (m : ) → p (m x)
      @[simp]
      theorem AddSubgroup.exists_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : { x // x AddSubgroup.zmultiples 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} [AddGroup G] {x : G} {p : GProp} :
      (g, g AddSubgroup.zmultiples x p g) m, p (m x)
      @[simp]
      theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ) :
      @[simp]
      theorem AddMonoidHom.map_zmultiples {G : Type u_1} [AddGroup G] {N : Type u_3} [AddGroup N] (f : G →+ N) (x : G) :
      @[simp]
      theorem MonoidHom.map_zpowers {G : Type u_1} [Group G] {N : Type u_3} [Group N] (f : G →* N) (x : G) :
      theorem ofMul_image_zpowers_eq_zmultiples_ofMul {G : Type u_1} [Group G] {x : G} :
      Additive.ofMul '' ↑(Subgroup.zpowers x) = ↑(AddSubgroup.zmultiples (Additive.ofMul x))
      theorem ofAdd_image_zmultiples_eq_zpowers_ofAdd {A : Type u_2} [AddGroup A] {x : A} :
      Multiplicative.ofAdd '' ↑(AddSubgroup.zmultiples x) = ↑(Subgroup.zpowers (Multiplicative.ofAdd x))
      abbrev AddSubgroup.zmultiples_isCommutative.match_1 {G : Type u_1} [AddGroup G] (g : G) (motive : { x // x AddSubgroup.zmultiples g }Prop) :
      (x : { x // x AddSubgroup.zmultiples g }) → ((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
      Instances For
        @[simp]
        theorem AddSubgroup.zmultiples_le {G : Type u_1} [AddGroup G] {g : G} {H : AddSubgroup G} :
        @[simp]
        theorem Subgroup.zpowers_le {G : Type u_1} [Group G] {g : G} {H : 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.

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

        Alias of the reverse direction of AddSubgroup.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} :
        theorem Subgroup.center_eq_iInf {G : Type u_1} [Group G] (S : Set G) (hS : Subgroup.closure S = ) :
        theorem Subgroup.center_eq_infi' {G : Type u_1} [Group G] (S : Set G) (hS : Subgroup.closure S = ) :