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
            noncomputable instance AddSubgroup.decidableMemZMultiples {G : Type u_1} [AddGroup G] {a : G} :
            DecidablePred fun (x : G) => x zmultiples 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]
              @[deprecated Subgroup.zpowers_isMulCommutative (since := "2025-04-09")]
              theorem Subgroup.zpowers_isCommutative {G : Type u_1} [Group G] (g : G) :

              Alias of Subgroup.zpowers_isMulCommutative.

              @[deprecated AddSubgroup.zmultiples_isAddCommutative (since := "2025-04-09")]

              Alias of AddSubgroup.zmultiples_isAddCommutative.

              @[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} :