Documentation

Mathlib.GroupTheory.Exponent

Exponent of a group #

This file defines the exponent of a group, or more generally a monoid. For a group G it is defined to be the minimal n≥1 such that g ^ n = 1 for all g ∈ G. For a finite group G, it is equal to the lowest common multiple of the order of all elements of the group G.

Main definitions #

Main results #

TODO #

A predicate on an additive monoid saying that there is a positive integer n such

that n • g = 0 for all g.

Equations
Instances For

    A predicate on a monoid saying that there is a positive integer n such that g ^ n = 1 for all g.

    Equations
    Instances For
      noncomputable def AddMonoid.exponent (G : Type u) [AddMonoid G] :

      The exponent of an additive group is the smallest positive integer n such that

      n • g = 0 for all g ∈ G if it exists, otherwise it is zero by convention.

      Equations
      Instances For
        noncomputable def Monoid.exponent (G : Type u) [Monoid G] :

        The exponent of a group is the smallest positive integer n such that g ^ n = 1 for all g ∈ G if it exists, otherwise it is zero by convention.

        Equations
        Instances For

          Alias of the reverse direction of Monoid.exponent_pos.

          theorem AddMonoid.exponent_eq_zero_iff_forall {G : Type u} [AddMonoid G] :
          AddMonoid.exponent G = 0 n > 0, ∃ (g : G), n g 0

          The exponent is zero iff for all nonzero n, one can find a g such that n • g ≠ 0.

          theorem Monoid.exponent_eq_zero_iff_forall {G : Type u} [Monoid G] :
          Monoid.exponent G = 0 n > 0, ∃ (g : G), g ^ n 1

          The exponent is zero iff for all nonzero n, one can find a g such that g ^ n ≠ 1.

          theorem Monoid.pow_exponent_eq_one {G : Type u} [Monoid G] (g : G) :
          theorem AddMonoid.nsmul_eq_mod_exponent {G : Type u} [AddMonoid G] {n : } (g : G) :
          theorem Monoid.pow_eq_mod_exponent {G : Type u} [Monoid G] {n : } (g : G) :
          g ^ n = g ^ (n % Monoid.exponent G)
          theorem AddMonoid.exponent_pos_of_exists {G : Type u} [AddMonoid G] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), n g = 0) :
          theorem Monoid.exponent_pos_of_exists {G : Type u} [Monoid G] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) :
          theorem AddMonoid.exponent_min' {G : Type u} [AddMonoid G] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), n g = 0) :
          theorem Monoid.exponent_min' {G : Type u} [Monoid G] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) :
          theorem AddMonoid.exponent_min {G : Type u} [AddMonoid G] (m : ) (hpos : 0 < m) (hm : m < AddMonoid.exponent G) :
          ∃ (g : G), m g 0
          theorem Monoid.exponent_min {G : Type u} [Monoid G] (m : ) (hpos : 0 < m) (hm : m < Monoid.exponent G) :
          ∃ (g : G), g ^ m 1
          theorem Monoid.exponent_dvd_iff_forall_pow_eq_one {G : Type u} [Monoid G] {n : } :
          Monoid.exponent G n ∀ (g : G), g ^ n = 1
          theorem Monoid.exponent_dvd_of_forall_pow_eq_one {G : Type u} [Monoid G] {n : } :
          (∀ (g : G), g ^ n = 1)Monoid.exponent G n

          Alias of the reverse direction of Monoid.exponent_dvd_iff_forall_pow_eq_one.

          theorem AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero {G : Type u} [AddMonoid G] {n : } :
          (∀ (g : G), n g = 0)AddMonoid.exponent G n
          theorem AddMonoid.exponent_dvd {G : Type u} [AddMonoid G] {n : } :
          AddMonoid.exponent G n ∀ (g : G), addOrderOf g n
          theorem Monoid.exponent_dvd {G : Type u} [Monoid G] {n : } :
          Monoid.exponent G n ∀ (g : G), orderOf g n
          @[deprecated]
          @[deprecated]
          theorem Monoid.exponent_dvd_of_forall_orderOf_dvd (G : Type u) [Monoid G] (n : ) (h : ∀ (g : G), orderOf g n) :
          theorem AddMonoid.lcm_addOrderOf_dvd_exponent (G : Type u) [AddMonoid G] [Fintype G] :
          Finset.univ.lcm addOrderOf AddMonoid.exponent G
          theorem Monoid.lcm_orderOf_dvd_exponent (G : Type u) [Monoid G] [Fintype G] :
          Finset.univ.lcm orderOf Monoid.exponent G
          theorem Nat.Prime.exists_orderOf_eq_pow_factorization_exponent (G : Type u) [Monoid G] {p : } (hp : Nat.Prime p) :
          ∃ (g : G), orderOf g = p ^ (Monoid.exponent G).factorization p
          theorem AddCommute.addOrderOf_add_nsmul_eq_lcm {G : Type u} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) (hx : addOrderOf x 0) (hy : addOrderOf y 0) :
          addOrderOf ((addOrderOf x / (addOrderOf x).factorizationLCMLeft (addOrderOf y)) x + (addOrderOf y / (addOrderOf x).factorizationLCMRight (addOrderOf y)) y) = (addOrderOf x).lcm (addOrderOf y)

          If two commuting elements x and y of an additive monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the sum of a multiple of x and a multiple of y. See also the result below if you don't need the explicit formula.

          theorem Commute.orderOf_mul_pow_eq_lcm {G : Type u} [Monoid G] {x : G} {y : G} (h : Commute x y) (hx : orderOf x 0) (hy : orderOf y 0) :
          orderOf (x ^ (orderOf x / (orderOf x).factorizationLCMLeft (orderOf y)) * y ^ (orderOf y / (orderOf x).factorizationLCMRight (orderOf y))) = (orderOf x).lcm (orderOf y)

          If two commuting elements x and y of a monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the product of a power of x and a power of y. See also the result below if you don't need the explicit formula.

          theorem AddCommute.exists_addOrderOf_eq_lcm (G : Type u) [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) :
          zAddSubmonoid.closure {x, y}, addOrderOf z = (addOrderOf x).lcm (addOrderOf y)

          If two commuting elements x and y of an additive monoid have order n and m, then there is an element of order lcm n m that lies in the additive subgroup generated by x and y.

          theorem Commute.exists_orderOf_eq_lcm (G : Type u) [Monoid G] {x : G} {y : G} (h : Commute x y) :
          zSubmonoid.closure {x, y}, orderOf z = (orderOf x).lcm (orderOf y)

          If two commuting elements x and y of a monoid have order n and m, then there is an element of order lcm n m that lies in the subgroup generated by x and y.

          theorem AddMonoid.exponent_eq_prime_iff {G : Type u_1} [AddMonoid G] [Nontrivial G] {p : } (hp : Nat.Prime p) :
          AddMonoid.exponent G = p ∀ (g : G), g 0addOrderOf g = p
          theorem Monoid.exponent_eq_prime_iff {G : Type u_1} [Monoid G] [Nontrivial G] {p : } (hp : Nat.Prime p) :
          Monoid.exponent G = p ∀ (g : G), g 1orderOf g = p

          A nontrivial monoid has prime exponent p if and only if every non-identity element has order p.

          theorem Monoid.exponent_ne_zero_iff_range_orderOf_finite {G : Type u} [Monoid G] (h : ∀ (g : G), 0 < orderOf g) :
          Monoid.exponent G 0 (Set.range orderOf).Finite
          theorem AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite {G : Type u} [AddMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) :
          AddMonoid.exponent G = 0 (Set.range addOrderOf).Infinite
          theorem Monoid.exponent_eq_zero_iff_range_orderOf_infinite {G : Type u} [Monoid G] (h : ∀ (g : G), 0 < orderOf g) :
          Monoid.exponent G = 0 (Set.range orderOf).Infinite
          theorem AddMonoid.lcm_addOrderOf_eq_exponent {G : Type u} [AddMonoid G] [Fintype G] :
          Finset.univ.lcm addOrderOf = AddMonoid.exponent G
          theorem Monoid.lcm_orderOf_eq_exponent {G : Type u} [Monoid G] [Fintype G] :
          Finset.univ.lcm orderOf = Monoid.exponent G
          @[deprecated]
          theorem Monoid.lcm_order_eq_exponent {G : Type u} [Monoid G] [Fintype G] :
          Finset.univ.lcm orderOf = Monoid.exponent G

          Alias of Monoid.lcm_orderOf_eq_exponent.

          @[deprecated]
          theorem AddMonoid.lcm_addOrder_eq_exponent {G : Type u} [AddMonoid G] [Fintype G] :
          Finset.univ.lcm addOrderOf = AddMonoid.exponent G

          If there exists an injective, addition-preserving map from G to H, then the exponent of G divides the exponent of H.

          theorem Monoid.exponent_dvd_of_monoidHom {G : Type u} [Monoid G] {H : Type u_1} [Monoid H] (e : G →* H) (e_inj : Function.Injective e) :

          If there exists an injective, multiplication-preserving map from G to H, then the exponent of G divides the exponent of H.

          If there exists a addition-preserving equivalence between G and H, then the exponent of G is equal to the exponent of H.

          theorem Monoid.exponent_eq_of_mulEquiv {G : Type u} [Monoid G] {H : Type u_1} [Monoid H] (e : G ≃* H) :

          If there exists a multiplication-preserving equivalence between G and H, then the exponent of G is equal to the exponent of H.

          theorem AddSubmonoid.nsmul_exponent_eq_zero {G : Type u} [AddMonoid G] {S : AddSubmonoid G} {g : G} (g_in_s : g S) :
          theorem Submonoid.pow_exponent_eq_one {G : Type u} [Monoid G] {S : Submonoid G} {g : G} (g_in_s : g S) :
          theorem AddMonoid.exponent_eq_iSup_addOrderOf {G : Type u} [AddCommMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) :
          theorem Monoid.exponent_eq_iSup_orderOf {G : Type u} [CommMonoid G] (h : ∀ (g : G), 0 < orderOf g) :
          Monoid.exponent G = ⨆ (g : G), orderOf g
          theorem AddMonoid.exponent_eq_iSup_addOrderOf' {G : Type u} [AddCommMonoid G] :
          AddMonoid.exponent G = if ∃ (g : G), addOrderOf g = 0 then 0 else ⨆ (g : G), addOrderOf g
          theorem Monoid.exponent_eq_iSup_orderOf' {G : Type u} [CommMonoid G] :
          Monoid.exponent G = if ∃ (g : G), orderOf g = 0 then 0 else ⨆ (g : G), orderOf g
          theorem Monoid.exponent_eq_max'_orderOf {G : Type u} [CancelCommMonoid G] [Fintype G] :
          Monoid.exponent G = (Finset.image orderOf Finset.univ).max'
          @[deprecated Monoid.one_lt_exponent]
          @[deprecated Monoid.one_lt_exponent]
          theorem Subgroup.exponent_toSubmonoid {G : Type u} [Group G] (H : Subgroup G) :
          Monoid.exponent H.toSubmonoid = Monoid.exponent H
          theorem AddSubgroup.nsmul_exponent_eq_zero {G : Type u} [AddGroup G] {H : AddSubgroup G} {g : G} (g_in_H : g H) :
          theorem Subgroup.pow_exponent_eq_one {G : Type u} [Group G] {H : Subgroup G} {g : G} (g_in_H : g H) :
          theorem AddMonoid.exponent_pi_eq_zero {ι : Type u_1} {M : ιType u_2} [(i : ι) → AddMonoid (M i)] {j : ι} (hj : AddMonoid.exponent (M j) = 0) :
          AddMonoid.exponent ((i : ι) → M i) = 0
          theorem Monoid.exponent_pi_eq_zero {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {j : ι} (hj : Monoid.exponent (M j) = 0) :
          Monoid.exponent ((i : ι) → M i) = 0
          theorem AddMonoidHom.exponent_dvd {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [AddMonoid M₁] [AddMonoid M₂] [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {f : F} (hf : Function.Surjective f) :
          theorem MonoidHom.exponent_dvd {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [Monoid M₁] [Monoid M₂] [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {f : F} (hf : Function.Surjective f) :

          If f : M₁ →⋆ M₂ is surjective, then the exponent of M₂ divides the exponent of M₁.

          theorem AddMonoid.exponent_pi {ι : Type u_1} [Fintype ι] {M : ιType u_2} [(i : ι) → AddMonoid (M i)] :
          AddMonoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun (x : ι) => AddMonoid.exponent (M x)

          The exponent of finite product of additive monoids is the Finset.lcm of the exponents of the constituent additive monoids.

          theorem Monoid.exponent_pi {ι : Type u_1} [Fintype ι] {M : ιType u_2} [(i : ι) → Monoid (M i)] :
          Monoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun (x : ι) => Monoid.exponent (M x)

          The exponent of finite product of monoids is the Finset.lcm of the exponents of the constituent monoids.

          theorem AddMonoid.exponent_prod {M₁ : Type u_1} {M₂ : Type u_2} [AddMonoid M₁] [AddMonoid M₂] :

          The exponent of product of two additive monoids is the lcm of the exponents of the individuaul additive monoids.

          theorem Monoid.exponent_prod {M₁ : Type u_1} {M₂ : Type u_2} [Monoid M₁] [Monoid M₂] :

          The exponent of product of two monoids is the lcm of the exponents of the individuaul monoids.

          Properties of monoids with exponent two #

          theorem addOrderOf_eq_two_iff {G : Type u} [AddMonoid G] (hG : AddMonoid.exponent G = 2) {x : G} :
          theorem orderOf_eq_two_iff {G : Type u} [Monoid G] (hG : Monoid.exponent G = 2) {x : G} :
          orderOf x = 2 x 1
          theorem AddCommute.of_addOrderOf_dvd_two {G : Type u} [AddMonoid G] [IsCancelAdd G] (h : ∀ (g : G), addOrderOf g 2) (a : G) (b : G) :
          theorem Commute.of_orderOf_dvd_two {G : Type u} [Monoid G] [IsCancelMul G] (h : ∀ (g : G), orderOf g 2) (a : G) (b : G) :
          theorem add_comm_of_exponent_two {G : Type u} [AddMonoid G] [IsCancelAdd G] (hG : AddMonoid.exponent G = 2) (a : G) (b : G) :
          a + b = b + a
          theorem mul_comm_of_exponent_two {G : Type u} [Monoid G] [IsCancelMul G] (hG : Monoid.exponent G = 2) (a : G) (b : G) :
          a * b = b * a

          In a cancellative monoid of exponent two, all elements commute.

          @[reducible, inline]

          Any additive group of exponent two is abelian.

          Equations
          Instances For
            @[reducible, inline]

            Any cancellative monoid of exponent two is abelian.

            Equations
            Instances For
              theorem neg_eq_self_of_exponent_two {G : Type u} [AddGroup G] (hG : AddMonoid.exponent G = 2) (x : G) :
              -x = x
              theorem inv_eq_self_of_exponent_two {G : Type u} [Group G] (hG : Monoid.exponent G = 2) (x : G) :
              x⁻¹ = x

              In a group of exponent two, every element is its own inverse.

              theorem neg_eq_self_of_addOrderOf_eq_two {G : Type u} [AddGroup G] {x : G} (hx : addOrderOf x = 2) :
              -x = x
              theorem inv_eq_self_of_orderOf_eq_two {G : Type u} [Group G] {x : G} (hx : orderOf x = 2) :
              x⁻¹ = x

              If an element in a group has order two, then it is its own inverse.

              theorem instAddCommGroupOfExponentTwo.proof_1 {G : Type u_1} [AddGroup G] (hG : AddMonoid.exponent G = 2) (a : G) (b : G) :
              a + b = b + a
              @[reducible, deprecated]

              Any additive group of exponent two is abelian.

              Equations
              Instances For
                @[reducible, deprecated]

                Any group of exponent two is abelian.

                Equations
                Instances For
                  theorem add_not_mem_of_addOrderOf_eq_two {G : Type u} [AddGroup G] {x : G} {y : G} (hx : addOrderOf x = 2) (hy : addOrderOf y = 2) (hxy : x y) :
                  x + y{x, y, 0}
                  theorem mul_not_mem_of_orderOf_eq_two {G : Type u} [Group G] {x : G} {y : G} (hx : orderOf x = 2) (hy : orderOf y = 2) (hxy : x y) :
                  x * y{x, y, 1}
                  theorem add_not_mem_of_exponent_two {G : Type u} [AddGroup G] (h : AddMonoid.exponent G = 2) {x : G} {y : G} (hx : x 0) (hy : y 0) (hxy : x y) :
                  x + y{x, y, 0}
                  theorem mul_not_mem_of_exponent_two {G : Type u} [Group G] (h : Monoid.exponent G = 2) {x : G} {y : G} (hx : x 1) (hy : y 1) (hxy : x y) :
                  x * y{x, y, 1}