Documentation

Mathlib.Algebra.Group.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
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
    noncomputable instance Subgroup.decidableMemZPowers {G : Type u_1} [Group G] {a : G} :
    Equations
    @[simp]
    theorem Subgroup.range_zpowersHom {G : Type u_1} [Group G] (g : G) :
    ((zpowersHom G) g).range = Subgroup.zpowers g
    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 : (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 : GProp} :
    (∀ gSubgroup.zpowers x, p g) ∀ (m : ), p (x ^ m)
    theorem Subgroup.exists_mem_zpowers {G : Type u_1} [Group G] {x : G} {p : GProp} :
    (∃ gSubgroup.zpowers x, p g) ∃ (m : ), p (x ^ m)
    Equations
    • =
    def AddSubgroup.zmultiples {A : Type u_2} [AddGroup A] (a : A) :

    The subgroup generated by an element.

    Equations
    Instances For
      @[simp]
      @[simp]
      theorem AddSubgroup.coe_zmultiples {G : Type u_1} [AddGroup G] (g : G) :
      (AddSubgroup.zmultiples g) = Set.range fun (x : ) => x g
      noncomputable instance AddSubgroup.decidableMemZMultiples {G : Type u_1} [AddGroup G] {a : G} :
      Equations
      theorem AddSubgroup.mem_zmultiples_iff {G : Type u_1} [AddGroup G] {g : G} {h : G} :
      h AddSubgroup.zmultiples g ∃ (k : ), k g = h
      @[simp]
      @[simp]
      @[simp]
      theorem AddSubgroup.forall_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : (AddSubgroup.zmultiples x)Prop} :
      (∀ (g : (AddSubgroup.zmultiples x)), p g) ∀ (m : ), p m x,
      theorem AddSubgroup.forall_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : GProp} :
      (∀ gAddSubgroup.zmultiples x, p g) ∀ (m : ), p (m x)
      @[simp]
      theorem AddSubgroup.exists_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : (AddSubgroup.zmultiples x)Prop} :
      (∃ (g : (AddSubgroup.zmultiples x)), p g) ∃ (m : ), p m x,
      theorem AddSubgroup.exists_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {p : GProp} :
      (∃ gAddSubgroup.zmultiples x, p g) ∃ (m : ), p (m x)
      @[simp]
      theorem AddSubgroup.intCast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ) :
      @[deprecated AddSubgroup.intCast_mul_mem_zmultiples]
      theorem AddSubgroup.int_cast_mul_mem_zmultiples {R : Type u_4} [Ring R] (r : R) (k : ) :

      Alias of AddSubgroup.intCast_mul_mem_zmultiples.

      @[deprecated AddSubgroup.intCast_mem_zmultiples_one]

      Alias of AddSubgroup.intCast_mem_zmultiples_one.

      @[simp]
      @[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))
      instance AddSubgroup.zmultiples_isCommutative {G : Type u_1} [AddGroup G] (g : G) :
      (AddSubgroup.zmultiples g).IsCommutative
      Equations
      • =
      instance Subgroup.zpowers_isCommutative {G : Type u_1} [Group G] (g : G) :
      (Subgroup.zpowers g).IsCommutative
      Equations
      • =
      @[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_infi' {G : Type u_1} [Group G] (S : Set G) (hS : Subgroup.closure S = ) :