Documentation

Mathlib.GroupTheory.OrderOfElement

Order of an element #

This file defines the order of an element of a finite group. For a finite group G the order of x ∈ G is the minimal n ≥ 1 such that x ^ n = 1.

Main definitions #

Tags #

order of an element

theorem isPeriodicPt_add_iff_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {n : } (x : G) :
Function.IsPeriodicPt (fun (x_1 : G) => x + x_1) n 0 n x = 0
theorem isPeriodicPt_mul_iff_pow_eq_one {G : Type u_1} [Monoid G] {n : } (x : G) :
Function.IsPeriodicPt (fun (x_1 : G) => x * x_1) n 1 x ^ n = 1
def IsOfFinAddOrder {G : Type u_1} [AddMonoid G] (x : G) :

IsOfFinAddOrder is a predicate on an element a of an additive monoid to be of finite order, i.e. there exists n ≥ 1 such that n • a = 0.

Equations
Instances For
    def IsOfFinOrder {G : Type u_1} [Monoid G] (x : G) :

    IsOfFinOrder is a predicate on an element x of a monoid to be of finite order, i.e. there exists n ≥ 1 such that x ^ n = 1.

    Equations
    Instances For
      theorem isOfFinAddOrder_ofMul_iff {G : Type u_1} [Monoid G] {x : G} :
      IsOfFinAddOrder (Additive.ofMul x) IsOfFinOrder x
      theorem isOfFinOrder_ofAdd_iff {α : Type u_6} [AddMonoid α] {x : α} :
      IsOfFinOrder (Multiplicative.ofAdd x) IsOfFinAddOrder x
      theorem isOfFinAddOrder_iff_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} :
      IsOfFinAddOrder x ∃ (n : ), 0 < n n x = 0
      theorem isOfFinOrder_iff_pow_eq_one {G : Type u_1} [Monoid G] {x : G} :
      IsOfFinOrder x ∃ (n : ), 0 < n x ^ n = 1
      theorem IsOfFinOrder.exists_pow_eq_one {G : Type u_1} [Monoid G] {x : G} :
      IsOfFinOrder x∃ (n : ), 0 < n x ^ n = 1

      Alias of the forward direction of isOfFinOrder_iff_pow_eq_one.

      theorem IsOfFinAddOrder.exists_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} :
      IsOfFinAddOrder x∃ (n : ), 0 < n n x = 0
      abbrev isOfFinAddOrder_iff_zsmul_eq_zero.match_1 {G : Type u_1} [AddGroup G] {x : G} (motive : (∃ (n : ), 0 < n n x = 0)Prop) :
      ∀ (x_1 : ∃ (n : ), 0 < n n x = 0), (∀ (n : ) (hn : 0 < n) (hn' : n x = 0), motive )motive x_1
      Equations
      • =
      Instances For
        theorem isOfFinAddOrder_iff_zsmul_eq_zero {G : Type u_6} [AddGroup G] {x : G} :
        IsOfFinAddOrder x ∃ (n : ), n 0 n x = 0
        abbrev isOfFinAddOrder_iff_zsmul_eq_zero.match_2 {G : Type u_1} [AddGroup G] {x : G} (motive : (∃ (n : ), n 0 n x = 0)Prop) :
        ∀ (x_1 : ∃ (n : ), n 0 n x = 0), (∀ (n : ) (hn : n 0) (hn' : n x = 0), motive )motive x_1
        Equations
        • =
        Instances For
          theorem isOfFinOrder_iff_zpow_eq_one {G : Type u_6} [Group G] {x : G} :
          IsOfFinOrder x ∃ (n : ), n 0 x ^ n = 1
          theorem IsOfFinOrder.pow {G : Type u_1} [Monoid G] {a : G} {n : } :

          Elements of finite order are of finite order in submonoids.

          theorem Submonoid.isOfFinOrder_coe {G : Type u_1} [Monoid G] {H : Submonoid G} {x : H} :

          Elements of finite order are of finite order in submonoids.

          theorem AddMonoidHom.isOfFinAddOrder {G : Type u_1} {H : Type u_2} [AddMonoid G] [AddMonoid H] (f : G →+ H) {x : G} (h : IsOfFinAddOrder x) :

          The image of an element of finite additive order has finite additive order.

          theorem MonoidHom.isOfFinOrder {G : Type u_1} {H : Type u_2} [Monoid G] [Monoid H] (f : G →* H) {x : G} (h : IsOfFinOrder x) :

          The image of an element of finite order has finite order.

          theorem IsOfFinAddOrder.apply {η : Type u_6} {Gs : ηType u_7} [(i : η) → AddMonoid (Gs i)] {x : (i : η) → Gs i} (h : IsOfFinAddOrder x) (i : η) :

          If a direct product has finite additive order then so does each component.

          theorem IsOfFinOrder.apply {η : Type u_6} {Gs : ηType u_7} [(i : η) → Monoid (Gs i)] {x : (i : η) → Gs i} (h : IsOfFinOrder x) (i : η) :

          If a direct product has finite order then so does each component.

          0 is of finite order in any additive monoid.

          theorem isOfFinOrder_one {G : Type u_1} [Monoid G] :

          1 is of finite order in any monoid.

          noncomputable abbrev IsOfFinAddOrder.addGroupMultiples {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) :

          The additive submonoid generated by an element is an additive group if that element has finite order.

          Equations
          Instances For
            theorem IsOfFinAddOrder.addGroupMultiples.proof_1 {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) :
            0 < .choose .choose x = 0
            @[reducible, inline]
            noncomputable abbrev IsOfFinOrder.groupPowers {G : Type u_1} [Monoid G] {x : G} (hx : IsOfFinOrder x) :

            The submonoid generated by an element is a group if that element has finite order.

            Equations
            Instances For
              noncomputable def addOrderOf {G : Type u_1} [AddMonoid G] (x : G) :

              addOrderOf a is the order of the element a, i.e. the n ≥ 1, s.t. n • a = 0 if it exists. Otherwise, i.e. if a is of infinite order, then addOrderOf a is 0 by convention.

              Equations
              Instances For
                noncomputable def orderOf {G : Type u_1} [Monoid G] (x : G) :

                orderOf x is the order of the element x, i.e. the n ≥ 1, s.t. x ^ n = 1 if it exists. Otherwise, i.e. if x is of infinite order, then orderOf x is 0 by convention.

                Equations
                Instances For
                  @[simp]
                  theorem addOrderOf_ofMul_eq_orderOf {G : Type u_1} [Monoid G] (x : G) :
                  addOrderOf (Additive.ofMul x) = orderOf x
                  @[simp]
                  theorem orderOf_ofAdd_eq_addOrderOf {α : Type u_6} [AddMonoid α] (a : α) :
                  orderOf (Multiplicative.ofAdd a) = addOrderOf a
                  theorem IsOfFinOrder.orderOf_pos {G : Type u_1} [Monoid G] {x : G} (h : IsOfFinOrder x) :
                  theorem addOrderOf_nsmul_eq_zero {G : Type u_1} [AddMonoid G] (x : G) :
                  theorem pow_orderOf_eq_one {G : Type u_1} [Monoid G] (x : G) :
                  x ^ orderOf x = 1
                  theorem addOrderOf_eq_zero {G : Type u_1} [AddMonoid G] {x : G} (h : ¬IsOfFinAddOrder x) :
                  theorem orderOf_eq_zero {G : Type u_1} [Monoid G] {x : G} (h : ¬IsOfFinOrder x) :
                  theorem orderOf_eq_zero_iff {G : Type u_1} [Monoid G] {x : G} :
                  theorem addOrderOf_eq_zero_iff' {G : Type u_1} [AddMonoid G] {x : G} :
                  addOrderOf x = 0 ∀ (n : ), 0 < nn x 0
                  theorem orderOf_eq_zero_iff' {G : Type u_1} [Monoid G] {x : G} :
                  orderOf x = 0 ∀ (n : ), 0 < nx ^ n 1
                  theorem addOrderOf_eq_iff {G : Type u_1} [AddMonoid G] {x : G} {n : } (h : 0 < n) :
                  addOrderOf x = n n x = 0 m < n, 0 < mm x 0
                  theorem orderOf_eq_iff {G : Type u_1} [Monoid G] {x : G} {n : } (h : 0 < n) :
                  orderOf x = n x ^ n = 1 m < n, 0 < mx ^ m 1
                  theorem addOrderOf_pos_iff {G : Type u_1} [AddMonoid G] {x : G} :

                  A group element has finite additive order iff its order is positive.

                  theorem orderOf_pos_iff {G : Type u_1} [Monoid G] {x : G} :

                  A group element has finite order iff its order is positive.

                  theorem IsOfFinAddOrder.mono {G : Type u_1} {β : Type u_5} [AddMonoid G] {x : G} [AddMonoid β] {y : β} (hx : IsOfFinAddOrder x) (h : addOrderOf y addOrderOf x) :
                  theorem IsOfFinOrder.mono {G : Type u_1} {β : Type u_5} [Monoid G] {x : G} [Monoid β] {y : β} (hx : IsOfFinOrder x) (h : orderOf y orderOf x) :
                  theorem nsmul_ne_zero_of_lt_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} {n : } (n0 : n 0) (h : n < addOrderOf x) :
                  n x 0
                  theorem pow_ne_one_of_lt_orderOf {G : Type u_1} [Monoid G] {x : G} {n : } (n0 : n 0) (h : n < orderOf x) :
                  x ^ n 1
                  @[deprecated pow_ne_one_of_lt_orderOf]
                  theorem pow_ne_one_of_lt_orderOf' {G : Type u_1} [Monoid G] {x : G} {n : } (n0 : n 0) (h : n < orderOf x) :
                  x ^ n 1

                  Alias of pow_ne_one_of_lt_orderOf.

                  @[deprecated nsmul_ne_zero_of_lt_addOrderOf]
                  theorem nsmul_ne_zero_of_lt_addOrderOf' {G : Type u_1} [AddMonoid G] {x : G} {n : } (n0 : n 0) (h : n < addOrderOf x) :
                  n x 0

                  Alias of nsmul_ne_zero_of_lt_addOrderOf.

                  theorem addOrderOf_le_of_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : } (hn : 0 < n) (h : n x = 0) :
                  theorem orderOf_le_of_pow_eq_one {G : Type u_1} [Monoid G] {x : G} {n : } (hn : 0 < n) (h : x ^ n = 1) :
                  @[simp]
                  theorem addOrderOf_zero {G : Type u_1} [AddMonoid G] :
                  @[simp]
                  theorem orderOf_one {G : Type u_1} [Monoid G] :
                  @[simp]
                  theorem AddMonoid.addOrderOf_eq_one_iff {G : Type u_1} [AddMonoid G] {x : G} :
                  addOrderOf x = 1 x = 0
                  @[simp]
                  theorem orderOf_eq_one_iff {G : Type u_1} [Monoid G] {x : G} :
                  orderOf x = 1 x = 1
                  @[simp]
                  theorem mod_addOrderOf_nsmul {G : Type u_1} [AddMonoid G] (x : G) (n : ) :
                  (n % addOrderOf x) x = n x
                  @[simp]
                  theorem pow_mod_orderOf {G : Type u_1} [Monoid G] (x : G) (n : ) :
                  x ^ (n % orderOf x) = x ^ n
                  theorem addOrderOf_dvd_of_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : } (h : n x = 0) :
                  theorem orderOf_dvd_of_pow_eq_one {G : Type u_1} [Monoid G] {x : G} {n : } (h : x ^ n = 1) :
                  theorem addOrderOf_dvd_iff_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : } :
                  addOrderOf x n n x = 0
                  theorem orderOf_dvd_iff_pow_eq_one {G : Type u_1} [Monoid G] {x : G} {n : } :
                  orderOf x n x ^ n = 1
                  theorem addOrderOf_smul_dvd {G : Type u_1} [AddMonoid G] {x : G} (n : ) :
                  theorem orderOf_pow_dvd {G : Type u_1} [Monoid G] {x : G} (n : ) :
                  theorem nsmul_injOn_Iio_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} :
                  Set.InjOn (fun (x_1 : ) => x_1 x) (Set.Iio (addOrderOf x))
                  theorem pow_injOn_Iio_orderOf {G : Type u_1} [Monoid G] {x : G} :
                  Set.InjOn (fun (x_1 : ) => x ^ x_1) (Set.Iio (orderOf x))
                  theorem IsOfFinOrder.mem_powers_iff_mem_range_orderOf {G : Type u_1} [Monoid G] {x : G} {y : G} [DecidableEq G] (hx : IsOfFinOrder x) :
                  y Submonoid.powers x y Finset.image (fun (x_1 : ) => x ^ x_1) (Finset.range (orderOf x))
                  theorem IsOfFinOrder.powers_eq_image_range_orderOf {G : Type u_1} [Monoid G] {x : G} [DecidableEq G] (hx : IsOfFinOrder x) :
                  (Submonoid.powers x) = (Finset.image (fun (x_1 : ) => x ^ x_1) (Finset.range (orderOf x)))
                  @[deprecated IsOfFinAddOrder.multiples_eq_image_range_addOrderOf]

                  Alias of IsOfFinAddOrder.multiples_eq_image_range_addOrderOf.

                  theorem nsmul_eq_zero_iff_modEq {G : Type u_1} [AddMonoid G] {x : G} {n : } :
                  n x = 0 n 0 [MOD addOrderOf x]
                  theorem pow_eq_one_iff_modEq {G : Type u_1} [Monoid G] {x : G} {n : } :
                  x ^ n = 1 n 0 [MOD orderOf x]
                  theorem addOrderOf_map_dvd {G : Type u_1} [AddMonoid G] {H : Type u_6} [AddMonoid H] (ψ : G →+ H) (x : G) :
                  theorem orderOf_map_dvd {G : Type u_1} [Monoid G] {H : Type u_6} [Monoid H] (ψ : G →* H) (x : G) :
                  theorem exists_nsmul_eq_self_of_coprime {G : Type u_1} [AddMonoid G] {x : G} {n : } (h : n.Coprime (addOrderOf x)) :
                  ∃ (m : ), m n x = x
                  theorem exists_pow_eq_self_of_coprime {G : Type u_1} [Monoid G] {x : G} {n : } (h : n.Coprime (orderOf x)) :
                  ∃ (m : ), (x ^ n) ^ m = x
                  theorem addOrderOf_eq_of_nsmul_and_div_prime_nsmul {G : Type u_1} [AddMonoid G] {x : G} {n : } (hn : 0 < n) (hx : n x = 0) (hd : ∀ (p : ), Nat.Prime pp n(n / p) x 0) :

                  If n * x = 0, but n/p * x ≠ 0 for all prime factors p of n, then x has order n in G.

                  theorem orderOf_eq_of_pow_and_pow_div_prime {G : Type u_1} [Monoid G] {x : G} {n : } (hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ (p : ), Nat.Prime pp nx ^ (n / p) 1) :

                  If x^n = 1, but x^(n/p) ≠ 1 for all prime factors p of n, then x has order n in G.

                  theorem addOrderOf_eq_addOrderOf_iff {G : Type u_1} [AddMonoid G] {x : G} {H : Type u_6} [AddMonoid H] {y : H} :
                  addOrderOf x = addOrderOf y ∀ (n : ), n x = 0 n y = 0
                  theorem orderOf_eq_orderOf_iff {G : Type u_1} [Monoid G] {x : G} {H : Type u_6} [Monoid H] {y : H} :
                  orderOf x = orderOf y ∀ (n : ), x ^ n = 1 y ^ n = 1
                  theorem addOrderOf_injective {G : Type u_1} [AddMonoid G] {H : Type u_6} [AddMonoid H] (f : G →+ H) (hf : Function.Injective f) (x : G) :

                  An injective homomorphism of additive monoids preserves orders of elements.

                  theorem orderOf_injective {G : Type u_1} [Monoid G] {H : Type u_6} [Monoid H] (f : G →* H) (hf : Function.Injective f) (x : G) :
                  orderOf (f x) = orderOf x

                  An injective homomorphism of monoids preserves orders of elements.

                  @[simp]
                  theorem AddEquiv.addOrderOf_eq {G : Type u_1} [AddMonoid G] {H : Type u_6} [AddMonoid H] (e : G ≃+ H) (x : G) :

                  An additive equivalence preserves orders of elements.

                  @[simp]
                  theorem MulEquiv.orderOf_eq {G : Type u_1} [Monoid G] {H : Type u_6} [Monoid H] (e : G ≃* H) (x : G) :
                  orderOf (e x) = orderOf x

                  A multiplicative equivalence preserves orders of elements.

                  theorem Function.Injective.isOfFinAddOrder_iff {G : Type u_1} {H : Type u_2} [AddMonoid G] {x : G} [AddMonoid H] {f : G →+ H} (hf : Function.Injective f) :
                  theorem Function.Injective.isOfFinOrder_iff {G : Type u_1} {H : Type u_2} [Monoid G] {x : G} [Monoid H] {f : G →* H} (hf : Function.Injective f) :
                  @[simp]
                  theorem addOrderOf_addSubmonoid {G : Type u_1} [AddMonoid G] {H : AddSubmonoid G} (y : H) :
                  @[simp]
                  theorem orderOf_submonoid {G : Type u_1} [Monoid G] {H : Submonoid G} (y : H) :
                  theorem orderOf_units {G : Type u_1} [Monoid G] {y : Gˣ} :
                  @[simp]
                  theorem IsOfFinOrder.val_inv_unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) :
                  hx.unit⁻¹ = x ^ (orderOf x - 1)
                  @[simp]
                  theorem IsOfFinOrder.val_unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) :
                  hx.unit = x
                  noncomputable def IsOfFinOrder.unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) :

                  If the order of x is finite, then x is a unit with inverse x ^ (orderOf x - 1).

                  Equations
                  • hx.unit = { val := x, inv := x ^ (orderOf x - 1), val_inv := , inv_val := }
                  Instances For
                    theorem IsOfFinOrder.isUnit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) :
                    theorem addOrderOf_nsmul' {G : Type u_1} [AddMonoid G] (x : G) {n : } (h : n 0) :
                    theorem orderOf_pow' {G : Type u_1} [Monoid G] (x : G) {n : } (h : n 0) :
                    orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
                    theorem addOrderOf_nsmul_of_dvd {G : Type u_1} [AddMonoid G] {x : G} {n : } (hn : n 0) (dvd : n addOrderOf x) :
                    theorem orderOf_pow_of_dvd {G : Type u_1} [Monoid G] {x : G} {n : } (hn : n 0) (dvd : n orderOf x) :
                    orderOf (x ^ n) = orderOf x / n
                    theorem addOrderOf_nsmul_addOrderOf_sub {G : Type u_1} [AddMonoid G] {x : G} {n : } (hx : addOrderOf x 0) (hn : n addOrderOf x) :
                    theorem orderOf_pow_orderOf_div {G : Type u_1} [Monoid G] {x : G} {n : } (hx : orderOf x 0) (hn : n orderOf x) :
                    orderOf (x ^ (orderOf x / n)) = n
                    theorem IsOfFinAddOrder.addOrderOf_nsmul {G : Type u_1} [AddMonoid G] (x : G) (n : ) (h : IsOfFinAddOrder x) :
                    theorem IsOfFinOrder.orderOf_pow {G : Type u_1} [Monoid G] (x : G) (n : ) (h : IsOfFinOrder x) :
                    orderOf (x ^ n) = orderOf x / (orderOf x).gcd n
                    theorem Nat.Coprime.addOrderOf_nsmul {G : Type u_1} [AddMonoid G] {y : G} {m : } (h : (addOrderOf y).Coprime m) :
                    theorem Nat.Coprime.orderOf_pow {G : Type u_1} [Monoid G] {y : G} {m : } (h : (orderOf y).Coprime m) :
                    orderOf (y ^ m) = orderOf y
                    theorem IsOfFinAddOrder.finite_multiples {G : Type u_1} [AddMonoid G] {a : G} (ha : IsOfFinAddOrder a) :
                    ((AddSubmonoid.multiples a)).Finite
                    theorem IsOfFinOrder.finite_powers {G : Type u_1} [Monoid G] {a : G} (ha : IsOfFinOrder a) :
                    ((Submonoid.powers a)).Finite
                    theorem AddCommute.addOrderOf_add_dvd_lcm {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) :
                    theorem Commute.orderOf_mul_dvd_lcm {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) :
                    orderOf (x * y) (orderOf x).lcm (orderOf y)
                    theorem AddCommute.addOrderOf_dvd_lcm_add {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) :
                    theorem Commute.orderOf_dvd_lcm_mul {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) :
                    orderOf y (orderOf x).lcm (orderOf (x * y))
                    theorem Commute.orderOf_mul_dvd_mul_orderOf {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) :
                    theorem AddCommute.addOrderOf_add_eq_mul_addOrderOf_of_coprime {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) (hco : (addOrderOf x).Coprime (addOrderOf y)) :
                    theorem Commute.orderOf_mul_eq_mul_orderOf_of_coprime {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) (hco : (orderOf x).Coprime (orderOf y)) :
                    theorem AddCommute.isOfFinAddOrder_add {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) (hx : IsOfFinAddOrder x) (hy : IsOfFinAddOrder y) :

                    Commuting elements of finite additive order are closed under addition.

                    theorem Commute.isOfFinOrder_mul {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) :

                    Commuting elements of finite order are closed under multiplication.

                    theorem AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) (hy : IsOfFinAddOrder y) (hdvd : ∀ (p : ), Nat.Prime pp addOrderOf xp * addOrderOf x addOrderOf y) :

                    If each prime factor of addOrderOf x has higher multiplicity in addOrderOf y, and x commutes with y, then x + y has the same order as y.

                    theorem Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) (hy : IsOfFinOrder y) (hdvd : ∀ (p : ), Nat.Prime pp orderOf xp * orderOf x orderOf y) :
                    orderOf (x * y) = orderOf y

                    If each prime factor of orderOf x has higher multiplicity in orderOf y, and x commutes with y, then x * y has the same order as y.

                    theorem addOrderOf_eq_prime {G : Type u_1} [AddMonoid G] {x : G} {p : } [hp : Fact (Nat.Prime p)] (hg : p x = 0) (hg1 : x 0) :
                    theorem orderOf_eq_prime {G : Type u_1} [Monoid G] {x : G} {p : } [hp : Fact (Nat.Prime p)] (hg : x ^ p = 1) (hg1 : x 1) :
                    theorem addOrderOf_eq_prime_pow {G : Type u_1} [AddMonoid G] {x : G} {n : } {p : } [hp : Fact (Nat.Prime p)] (hnot : ¬p ^ n x = 0) (hfin : p ^ (n + 1) x = 0) :
                    addOrderOf x = p ^ (n + 1)
                    theorem orderOf_eq_prime_pow {G : Type u_1} [Monoid G] {x : G} {n : } {p : } [hp : Fact (Nat.Prime p)] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :
                    orderOf x = p ^ (n + 1)
                    abbrev exists_addOrderOf_eq_prime_pow_iff.match_2 {G : Type u_1} [AddMonoid G] {x : G} {p : } (motive : (∃ (m : ), p ^ m x = 0)Prop) :
                    ∀ (x_1 : ∃ (m : ), p ^ m x = 0), (∀ (w : ) (hm : p ^ w x = 0), motive )motive x_1
                    Equations
                    • =
                    Instances For
                      abbrev exists_addOrderOf_eq_prime_pow_iff.match_1 {G : Type u_1} [AddMonoid G] {x : G} {p : } (motive : (∃ (k : ), addOrderOf x = p ^ k)Prop) :
                      ∀ (x_1 : ∃ (k : ), addOrderOf x = p ^ k), (∀ (k : ) (hk : addOrderOf x = p ^ k), motive )motive x_1
                      Equations
                      • =
                      Instances For
                        theorem exists_addOrderOf_eq_prime_pow_iff {G : Type u_1} [AddMonoid G] {x : G} {p : } [hp : Fact (Nat.Prime p)] :
                        (∃ (k : ), addOrderOf x = p ^ k) ∃ (m : ), p ^ m x = 0
                        theorem exists_orderOf_eq_prime_pow_iff {G : Type u_1} [Monoid G] {x : G} {p : } [hp : Fact (Nat.Prime p)] :
                        (∃ (k : ), orderOf x = p ^ k) ∃ (m : ), x ^ p ^ m = 1
                        theorem nsmul_eq_nsmul_iff_modEq {G : Type u_1} [AddLeftCancelMonoid G] {x : G} {m : } {n : } :
                        n x = m x n m [MOD addOrderOf x]
                        theorem pow_eq_pow_iff_modEq {G : Type u_1} [LeftCancelMonoid G] {x : G} {m : } {n : } :
                        x ^ n = x ^ m n m [MOD orderOf x]
                        @[simp]
                        theorem nsmul_inj_mod {G : Type u_1} [AddLeftCancelMonoid G] {x : G} {n : } {m : } :
                        n x = m x n % addOrderOf x = m % addOrderOf x
                        theorem pow_inj_mod {G : Type u_1} [LeftCancelMonoid G] {x : G} {n : } {m : } :
                        x ^ n = x ^ m n % orderOf x = m % orderOf x
                        theorem nsmul_inj_iff_of_addOrderOf_eq_zero {G : Type u_1} [AddLeftCancelMonoid G] {x : G} (h : addOrderOf x = 0) {n : } {m : } :
                        n x = m x n = m
                        theorem pow_inj_iff_of_orderOf_eq_zero {G : Type u_1} [LeftCancelMonoid G] {x : G} (h : orderOf x = 0) {n : } {m : } :
                        x ^ n = x ^ m n = m
                        theorem infinite_not_isOfFinAddOrder {G : Type u_1} [AddLeftCancelMonoid G] {x : G} (h : ¬IsOfFinAddOrder x) :
                        {y : G | ¬IsOfFinAddOrder y}.Infinite
                        theorem infinite_not_isOfFinOrder {G : Type u_1} [LeftCancelMonoid G] {x : G} (h : ¬IsOfFinOrder x) :
                        {y : G | ¬IsOfFinOrder y}.Infinite
                        @[simp]
                        theorem finite_multiples {G : Type u_1} [AddLeftCancelMonoid G] {a : G} :
                        @[simp]
                        theorem finite_powers {G : Type u_1} [LeftCancelMonoid G] {a : G} :
                        @[simp]
                        theorem infinite_multiples {G : Type u_1} [AddLeftCancelMonoid G] {a : G} :
                        @[simp]
                        theorem infinite_powers {G : Type u_1} [LeftCancelMonoid G] {a : G} :
                        ((Submonoid.powers a)).Infinite ¬IsOfFinOrder a
                        abbrev finEquivMultiples.match_3 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (motive : (AddSubmonoid.multiples x)Prop) :
                        ∀ (x_1 : (AddSubmonoid.multiples x)), (∀ (i : ), motive (fun (x_2 : ) => x_2 x) i, )motive x_1
                        Equations
                        • =
                        Instances For
                          abbrev finEquivMultiples.match_1 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) :
                          ∀ (val : ) (h₁ : val < addOrderOf x) (motive : (x_1 : Fin (addOrderOf x)) → (fun (n : Fin (addOrderOf x)) => n x, ) val, h₁ = (fun (n : Fin (addOrderOf x)) => n x, ) x_1Prop) (x_1 : Fin (addOrderOf x)) (ij : (fun (n : Fin (addOrderOf x)) => n x, ) val, h₁ = (fun (n : Fin (addOrderOf x)) => n x, ) x_1), (∀ (val_1 : ) (h₂ : val_1 < addOrderOf x) (ij : (fun (n : Fin (addOrderOf x)) => n x, ) val, h₁ = (fun (n : Fin (addOrderOf x)) => n x, ) val_1, h₂), motive val_1, h₂ ij)motive x_1 ij
                          Equations
                          • =
                          Instances For
                            noncomputable def finEquivMultiples {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (hx : IsOfFinAddOrder x) :

                            The equivalence between Fin (addOrderOf a) and AddSubmonoid.multiples a, sending i to i • a.

                            Equations
                            Instances For
                              theorem finEquivMultiples.proof_2 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (hx : IsOfFinAddOrder x) :
                              (Function.Injective fun (n : Fin (addOrderOf x)) => n x, ) Function.Surjective fun (n : Fin (addOrderOf x)) => n x,
                              theorem finEquivMultiples.proof_1 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (n : Fin (addOrderOf x)) :
                              ∃ (y : ), (fun (x_1 : ) => x_1 x) y = n x
                              abbrev finEquivMultiples.match_2 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) :
                              ∀ (x_1 : Fin (addOrderOf x)) (motive : (x_2 : Fin (addOrderOf x)) → (fun (n : Fin (addOrderOf x)) => n x, ) x_2 = (fun (n : Fin (addOrderOf x)) => n x, ) x_1Prop) (x_2 : Fin (addOrderOf x)) (ij : (fun (n : Fin (addOrderOf x)) => n x, ) x_2 = (fun (n : Fin (addOrderOf x)) => n x, ) x_1), (∀ (val : ) (h₁ : val < addOrderOf x) (ij : (fun (n : Fin (addOrderOf x)) => n x, ) val, h₁ = (fun (n : Fin (addOrderOf x)) => n x, ) x_1), motive val, h₁ ij)motive x_2 ij
                              Equations
                              • =
                              Instances For
                                noncomputable def finEquivPowers {G : Type u_1} [LeftCancelMonoid G] (x : G) (hx : IsOfFinOrder x) :

                                The equivalence between Fin (orderOf x) and Submonoid.powers x, sending i to x ^ i."

                                Equations
                                Instances For
                                  @[simp]
                                  theorem finEquivMultiples_apply {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (hx : IsOfFinAddOrder x) {n : Fin (addOrderOf x)} :
                                  (finEquivMultiples x hx) n = n x,
                                  @[simp]
                                  theorem finEquivPowers_apply {G : Type u_1} [LeftCancelMonoid G] (x : G) (hx : IsOfFinOrder x) {n : Fin (orderOf x)} :
                                  (finEquivPowers x hx) n = x ^ n,
                                  @[simp]
                                  theorem finEquivMultiples_symm_apply {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (hx : IsOfFinAddOrder x) (n : ) {hn : ∃ (m : ), m x = n x} :
                                  (finEquivMultiples x hx).symm n x, hn = n % addOrderOf x,
                                  @[simp]
                                  theorem finEquivPowers_symm_apply {G : Type u_1} [LeftCancelMonoid G] (x : G) (hx : IsOfFinOrder x) (n : ) {hn : ∃ (m : ), x ^ m = x ^ n} :
                                  (finEquivPowers x hx).symm x ^ n, hn = n % orderOf x,

                                  See also addOrder_eq_card_multiples.

                                  @[simp]

                                  Inverses of elements of finite additive order have finite additive order.

                                  @[simp]

                                  Inverses of elements of finite order have finite order.

                                  theorem IsOfFinOrder.inv {G : Type u_1} [Group G] {x : G} :

                                  Alias of the reverse direction of isOfFinOrder_inv_iff.


                                  Inverses of elements of finite order have finite order.

                                  theorem IsOfFinOrder.of_inv {G : Type u_1} [Group G] {x : G} :

                                  Alias of the forward direction of isOfFinOrder_inv_iff.


                                  Inverses of elements of finite order have finite order.

                                  theorem addOrderOf_dvd_iff_zsmul_eq_zero {G : Type u_1} [AddGroup G] {x : G} {i : } :
                                  (addOrderOf x) i i x = 0
                                  theorem orderOf_dvd_iff_zpow_eq_one {G : Type u_1} [Group G] {x : G} {i : } :
                                  (orderOf x) i x ^ i = 1
                                  @[simp]
                                  theorem addOrderOf_neg {G : Type u_1} [AddGroup G] (x : G) :
                                  @[simp]
                                  theorem orderOf_inv {G : Type u_1} [Group G] (x : G) :
                                  theorem AddSubgroup.addOrderOf_coe {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (a : H) :
                                  theorem Subgroup.orderOf_coe {G : Type u_1} [Group G] {H : Subgroup G} (a : H) :
                                  @[simp]
                                  theorem AddSubgroup.addOrderOf_mk {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (a : G) (ha : a H) :
                                  addOrderOf a, ha = addOrderOf a
                                  @[simp]
                                  theorem Subgroup.orderOf_mk {G : Type u_1} [Group G] {H : Subgroup G} (a : G) (ha : a H) :
                                  orderOf a, ha = orderOf a
                                  theorem mod_addOrderOf_zsmul {G : Type u_1} [AddGroup G] (x : G) (z : ) :
                                  (z % (addOrderOf x)) x = z x
                                  theorem zpow_mod_orderOf {G : Type u_1} [Group G] (x : G) (z : ) :
                                  x ^ (z % (orderOf x)) = x ^ z
                                  @[simp]
                                  theorem zsmul_smul_addOrderOf {G : Type u_1} [AddGroup G] {x : G} {i : } :
                                  @[simp]
                                  theorem zpow_pow_orderOf {G : Type u_1} [Group G] {x : G} {i : } :
                                  (x ^ i) ^ orderOf x = 1
                                  theorem IsOfFinAddOrder.zsmul {G : Type u_1} [AddGroup G] {x : G} (h : IsOfFinAddOrder x) {i : } :
                                  theorem IsOfFinOrder.zpow {G : Type u_1} [Group G] {x : G} (h : IsOfFinOrder x) {i : } :
                                  theorem IsOfFinOrder.of_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} (h : IsOfFinOrder x) (h' : y Subgroup.zpowers x) :
                                  theorem orderOf_dvd_of_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} (h : y Subgroup.zpowers x) :
                                  theorem smul_eq_self_of_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} {α : Type u_6} [MulAction G α] (hx : x Subgroup.zpowers y) {a : α} (hs : y a = a) :
                                  x a = a
                                  theorem vadd_eq_self_of_mem_zmultiples {α : Type u_6} {G : Type u_7} [AddGroup G] [AddAction G α] {x : G} {y : G} (hx : x AddSubgroup.zmultiples y) {a : α} (hs : y +ᵥ a = a) :
                                  x +ᵥ a = a
                                  abbrev IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples.match_2 {G : Type u_1} [AddGroup G] {x : G} {y : G} (motive : y AddSubgroup.zmultiples xProp) :
                                  ∀ (x_1 : y AddSubgroup.zmultiples x), (∀ (i : ) (hi : (fun (x_2 : ) => x_2 x) i = y), motive )motive x_1
                                  Equations
                                  • =
                                  Instances For
                                    abbrev IsOfFinAddOrder.mem_multiples_iff_mem_zmultiples.match_1 {G : Type u_1} [AddGroup G] {x : G} {y : G} (motive : y AddSubmonoid.multiples xProp) :
                                    ∀ (x_1 : y AddSubmonoid.multiples x), (∀ (n : ) (hn : (fun (x_2 : ) => x_2 x) n = y), motive )motive x_1
                                    Equations
                                    • =
                                    Instances For
                                      theorem IsOfFinOrder.powers_eq_zpowers {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) :
                                      theorem IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf {G : Type u_1} [Group G] {x : G} {y : G} [DecidableEq G] (hx : IsOfFinOrder x) :
                                      y Subgroup.zpowers x y Finset.image (fun (x_1 : ) => x ^ x_1) (Finset.range (orderOf x))
                                      noncomputable def finEquivZMultiples {G : Type u_1} [AddGroup G] (x : G) (hx : IsOfFinAddOrder x) :

                                      The equivalence between Fin (addOrderOf a) and Subgroup.zmultiples a, sending i to i • a.

                                      Equations
                                      Instances For
                                        noncomputable def finEquivZPowers {G : Type u_1} [Group G] (x : G) (hx : IsOfFinOrder x) :

                                        The equivalence between Fin (orderOf x) and Subgroup.zpowers x, sending i to x ^ i.

                                        Equations
                                        Instances For
                                          @[simp]
                                          theorem finEquivZMultiples_apply {G : Type u_1} [AddGroup G] {x : G} (hx : IsOfFinAddOrder x) {n : Fin (addOrderOf x)} :
                                          (finEquivZMultiples x hx) n = n x,
                                          @[simp]
                                          theorem finEquivZPowers_apply {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)} :
                                          (finEquivZPowers x hx) n = x ^ n,
                                          @[simp]
                                          theorem finEquivZMultiples_symm_apply {G : Type u_1} [AddGroup G] (x : G) (hx : IsOfFinAddOrder x) (n : ) :
                                          (finEquivZMultiples x hx).symm n x, = n % addOrderOf x,
                                          @[simp]
                                          theorem finEquivZPowers_symm_apply {G : Type u_1} [Group G] (x : G) (hx : IsOfFinOrder x) (n : ) :
                                          (finEquivZPowers x hx).symm x ^ n, = n % orderOf x,
                                          theorem IsOfFinAddOrder.add {G : Type u_1} [AddCommMonoid G] {x : G} {y : G} (hx : IsOfFinAddOrder x) (hy : IsOfFinAddOrder y) :

                                          Elements of finite additive order are closed under addition.

                                          theorem IsOfFinOrder.mul {G : Type u_1} [CommMonoid G] {x : G} {y : G} (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) :

                                          Elements of finite order are closed under multiplication.

                                          abbrev sum_card_addOrderOf_eq_card_nsmul_eq_zero.match_1 {G : Type u_1} [AddMonoid G] {n : } (x : G) (motive : addOrderOf x nProp) :
                                          ∀ (x_1 : addOrderOf x n), (∀ (m : ) (hm : n = addOrderOf x * m), motive )motive x_1
                                          Equations
                                          • =
                                          Instances For
                                            theorem sum_card_addOrderOf_eq_card_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {n : } [Fintype G] [DecidableEq G] (hn : n 0) :
                                            mFinset.filter (fun (x : ) => x n) (Finset.range n.succ), (Finset.filter (fun (x : G) => addOrderOf x = m) Finset.univ).card = (Finset.filter (fun (x : G) => n x = 0) Finset.univ).card
                                            theorem sum_card_orderOf_eq_card_pow_eq_one {G : Type u_1} [Monoid G] {n : } [Fintype G] [DecidableEq G] (hn : n 0) :
                                            mFinset.filter (fun (x : ) => x n) (Finset.range n.succ), (Finset.filter (fun (x : G) => orderOf x = m) Finset.univ).card = (Finset.filter (fun (x : G) => x ^ n = 1) Finset.univ).card
                                            theorem orderOf_le_card_univ {G : Type u_1} [Monoid G] {x : G} [Fintype G] :
                                            theorem addOrderOf_pos {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) :

                                            This is the same as IsOfFinAddOrder.addOrderOf_pos but with one fewer explicit assumption since this is automatic in case of a finite cancellative additive monoid.

                                            theorem orderOf_pos {G : Type u_1} [LeftCancelMonoid G] [Finite G] (x : G) :

                                            This is the same as IsOfFinOrder.orderOf_pos but with one fewer explicit assumption since this is automatic in case of a finite cancellative monoid.

                                            theorem addOrderOf_nsmul {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {n : } (x : G) :

                                            This is the same as addOrderOf_nsmul' and addOrderOf_nsmul but with one assumption less which is automatic in the case of a finite cancellative additive monoid.

                                            theorem orderOf_pow {G : Type u_1} [LeftCancelMonoid G] [Finite G] {n : } (x : G) :
                                            orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

                                            This is the same as orderOf_pow' and orderOf_pow'' but with one assumption less which is automatic in the case of a finite cancellative monoid.

                                            theorem mem_powers_iff_mem_range_orderOf {G : Type u_1} [LeftCancelMonoid G] [Finite G] {x : G} {y : G} [DecidableEq G] :
                                            y Submonoid.powers x y Finset.image (fun (x_1 : ) => x ^ x_1) (Finset.range (orderOf x))
                                            noncomputable def multiplesEquivMultiples {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {x : G} {y : G} (h : addOrderOf x = addOrderOf y) :

                                            The equivalence between Submonoid.multiples of two elements a, b of the same additive order, mapping i • a to i • b.

                                            Equations
                                            Instances For
                                              noncomputable def powersEquivPowers {G : Type u_1} [LeftCancelMonoid G] [Finite G] {x : G} {y : G} (h : orderOf x = orderOf y) :

                                              The equivalence between Submonoid.powers of two elements x, y of the same order, mapping x ^ i to y ^ i.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem multiplesEquivMultiples_apply {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {x : G} {y : G} (h : addOrderOf x = addOrderOf y) (n : ) :
                                                (multiplesEquivMultiples h) n x, = n y,
                                                @[simp]
                                                theorem powersEquivPowers_apply {G : Type u_1} [LeftCancelMonoid G] [Finite G] {x : G} {y : G} (h : orderOf x = orderOf y) (n : ) :
                                                (powersEquivPowers h) x ^ n, = y ^ n,
                                                theorem exists_zsmul_eq_zero {G : Type u_1} [AddGroup G] [Finite G] (x : G) :
                                                ∃ (i : ) (_ : i 0), i x = 0
                                                theorem exists_zpow_eq_one {G : Type u_1} [Group G] [Finite G] (x : G) :
                                                ∃ (i : ) (_ : i 0), x ^ i = 1
                                                theorem mem_powers_iff_mem_zpowers {G : Type u_1} [Group G] [Finite G] {x : G} {y : G} :
                                                theorem powers_eq_zpowers {G : Type u_1} [Group G] [Finite G] (x : G) :
                                                theorem mem_zpowers_iff_mem_range_orderOf {G : Type u_1} [Group G] [Finite G] {x : G} {y : G} [DecidableEq G] :
                                                y Subgroup.zpowers x y Finset.image (fun (x_1 : ) => x ^ x_1) (Finset.range (orderOf x))
                                                theorem zsmul_eq_zero_iff_modEq {G : Type u_1} [AddGroup G] {x : G} {n : } :
                                                n x = 0 n 0 [ZMOD (addOrderOf x)]
                                                theorem zpow_eq_one_iff_modEq {G : Type u_1} [Group G] {x : G} {n : } :
                                                x ^ n = 1 n 0 [ZMOD (orderOf x)]
                                                theorem zsmul_eq_zsmul_iff_modEq {G : Type u_1} [AddGroup G] {x : G} {m : } {n : } :
                                                m x = n x m n [ZMOD (addOrderOf x)]
                                                theorem zpow_eq_zpow_iff_modEq {G : Type u_1} [Group G] {x : G} {m : } {n : } :
                                                x ^ m = x ^ n m n [ZMOD (orderOf x)]
                                                @[simp]
                                                theorem injective_zpow_iff_not_isOfFinOrder {G : Type u_1} [Group G] {x : G} :
                                                noncomputable def zmultiplesEquivZMultiples {G : Type u_1} [AddGroup G] [Finite G] {x : G} {y : G} (h : addOrderOf x = addOrderOf y) :

                                                The equivalence between Subgroup.zmultiples of two elements a, b of the same additive order, mapping i • a to i • b.

                                                Equations
                                                Instances For
                                                  noncomputable def zpowersEquivZPowers {G : Type u_1} [Group G] [Finite G] {x : G} {y : G} (h : orderOf x = orderOf y) :

                                                  The equivalence between Subgroup.zpowers of two elements x, y of the same order, mapping x ^ i to y ^ i.

                                                  Equations
                                                  Instances For
                                                    @[simp]
                                                    theorem zmultiples_equiv_zmultiples_apply {G : Type u_1} [AddGroup G] [Finite G] {x : G} {y : G} (h : addOrderOf x = addOrderOf y) (n : ) :
                                                    (zmultiplesEquivZMultiples h) n x, = n y,
                                                    @[simp]
                                                    theorem zpowersEquivZPowers_apply {G : Type u_1} [Group G] [Finite G] {x : G} {y : G} (h : orderOf x = orderOf y) (n : ) :
                                                    (zpowersEquivZPowers h) x ^ n, = y ^ n,

                                                    See also Nat.card_subgroup.

                                                    theorem Fintype.card_zpowers {G : Type u_1} [Group G] [Fintype G] {x : G} :

                                                    See also Nat.card_addSubgroupZPowers.

                                                    theorem card_zmultiples_le {G : Type u_1} [AddGroup G] [Fintype G] (a : G) {k : } (k_pos : k 0) (ha : k a = 0) :
                                                    theorem card_zpowers_le {G : Type u_1} [Group G] [Fintype G] (a : G) {k : } (k_pos : k 0) (ha : a ^ k = 1) :
                                                    theorem orderOf_dvd_card {G : Type u_1} [Group G] [Fintype G] {x : G} :
                                                    theorem orderOf_dvd_natCard {G : Type u_6} [Group G] (x : G) :
                                                    theorem AddSubgroup.addOrderOf_dvd_natCard {G : Type u_1} [AddGroup G] {x : G} (s : AddSubgroup G) (hx : x s) :
                                                    theorem Subgroup.orderOf_dvd_natCard {G : Type u_1} [Group G] {x : G} (s : Subgroup G) (hx : x s) :
                                                    theorem AddSubgroup.addOrderOf_le_card {G : Type u_1} [AddGroup G] {x : G} (s : AddSubgroup G) (hs : (s).Finite) (hx : x s) :
                                                    theorem Subgroup.orderOf_le_card {G : Type u_1} [Group G] {x : G} (s : Subgroup G) (hs : (s).Finite) (hx : x s) :
                                                    theorem AddSubmonoid.addOrderOf_le_card {G : Type u_1} [AddGroup G] {x : G} (s : AddSubmonoid G) (hs : (s).Finite) (hx : x s) :
                                                    theorem Submonoid.orderOf_le_card {G : Type u_1} [Group G] {x : G} (s : Submonoid G) (hs : (s).Finite) (hx : x s) :
                                                    @[simp]
                                                    theorem card_nsmul_eq_zero' {G : Type u_6} [AddGroup G] {x : G} :
                                                    Nat.card G x = 0
                                                    @[simp]
                                                    theorem pow_card_eq_one' {G : Type u_6} [Group G] {x : G} :
                                                    x ^ Nat.card G = 1
                                                    @[simp]
                                                    theorem card_nsmul_eq_zero {G : Type u_1} [AddGroup G] [Fintype G] {x : G} :
                                                    @[simp]
                                                    theorem pow_card_eq_one {G : Type u_1} [Group G] [Fintype G] {x : G} :
                                                    theorem AddSubgroup.nsmul_index_mem {G : Type u_6} [AddGroup G] (H : AddSubgroup G) [H.Normal] (g : G) :
                                                    H.index g H
                                                    theorem Subgroup.pow_index_mem {G : Type u_6} [Group G] (H : Subgroup G) [H.Normal] (g : G) :
                                                    g ^ H.index H
                                                    @[simp]
                                                    theorem mod_card_nsmul {G : Type u_1} [AddGroup G] [Fintype G] (a : G) (n : ) :
                                                    (n % Fintype.card G) a = n a
                                                    @[simp]
                                                    theorem pow_mod_card {G : Type u_1} [Group G] [Fintype G] (a : G) (n : ) :
                                                    a ^ (n % Fintype.card G) = a ^ n
                                                    @[simp]
                                                    theorem mod_card_zsmul {G : Type u_1} [AddGroup G] [Fintype G] (a : G) (n : ) :
                                                    (n % (Fintype.card G)) a = n a
                                                    @[simp]
                                                    theorem zpow_mod_card {G : Type u_1} [Group G] [Fintype G] (a : G) (n : ) :
                                                    a ^ (n % (Fintype.card G)) = a ^ n
                                                    @[simp]
                                                    theorem mod_natCard_nsmul {G : Type u_1} [AddGroup G] (a : G) (n : ) :
                                                    (n % Nat.card G) a = n a
                                                    @[simp]
                                                    theorem pow_mod_natCard {G : Type u_1} [Group G] (a : G) (n : ) :
                                                    a ^ (n % Nat.card G) = a ^ n
                                                    @[simp]
                                                    theorem mod_natCard_zsmul {G : Type u_1} [AddGroup G] (a : G) (n : ) :
                                                    (n % (Nat.card G)) a = n a
                                                    @[simp]
                                                    theorem zpow_mod_natCard {G : Type u_1} [Group G] (a : G) (n : ) :
                                                    a ^ (n % (Nat.card G)) = a ^ n
                                                    theorem nsmulCoprime.proof_1 {n : } {G : Type u_1} [AddGroup G] (h : (Nat.card G).Coprime n) (g : G) :
                                                    (fun (g : G) => (Nat.card G).gcdB n g) ((fun (g : G) => n g) g) = g
                                                    noncomputable def nsmulCoprime {n : } {G : Type u_6} [AddGroup G] (h : (Nat.card G).Coprime n) :
                                                    G G

                                                    If gcd(|G|,n)=1 then the smul by n is a bijection

                                                    Equations
                                                    • nsmulCoprime h = { toFun := fun (g : G) => n g, invFun := fun (g : G) => (Nat.card G).gcdB n g, left_inv := , right_inv := }
                                                    Instances For
                                                      theorem nsmulCoprime.proof_2 {n : } {G : Type u_1} [AddGroup G] (h : (Nat.card G).Coprime n) (g : G) :
                                                      (fun (g : G) => n g) ((fun (g : G) => (Nat.card G).gcdB n g) g) = g
                                                      @[simp]
                                                      theorem nsmulCoprime_symm_apply {n : } {G : Type u_6} [AddGroup G] (h : (Nat.card G).Coprime n) (g : G) :
                                                      (nsmulCoprime h).symm g = (Nat.card G).gcdB n g
                                                      @[simp]
                                                      theorem powCoprime_symm_apply {n : } {G : Type u_6} [Group G] (h : (Nat.card G).Coprime n) (g : G) :
                                                      (powCoprime h).symm g = g ^ (Nat.card G).gcdB n
                                                      @[simp]
                                                      theorem powCoprime_apply {n : } {G : Type u_6} [Group G] (h : (Nat.card G).Coprime n) (g : G) :
                                                      (powCoprime h) g = g ^ n
                                                      @[simp]
                                                      theorem nsmulCoprime_apply {n : } {G : Type u_6} [AddGroup G] (h : (Nat.card G).Coprime n) (g : G) :
                                                      (nsmulCoprime h) g = n g
                                                      noncomputable def powCoprime {n : } {G : Type u_6} [Group G] (h : (Nat.card G).Coprime n) :
                                                      G G

                                                      If gcd(|G|,n)=1 then the nth power map is a bijection

                                                      Equations
                                                      • powCoprime h = { toFun := fun (g : G) => g ^ n, invFun := fun (g : G) => g ^ (Nat.card G).gcdB n, left_inv := , right_inv := }
                                                      Instances For
                                                        theorem nsmulCoprime_zero {n : } {G : Type u_6} [AddGroup G] (h : (Nat.card G).Coprime n) :
                                                        (nsmulCoprime h) 0 = 0
                                                        theorem powCoprime_one {n : } {G : Type u_6} [Group G] (h : (Nat.card G).Coprime n) :
                                                        (powCoprime h) 1 = 1
                                                        theorem nsmulCoprime_neg {n : } {G : Type u_6} [AddGroup G] (h : (Nat.card G).Coprime n) {g : G} :
                                                        theorem powCoprime_inv {n : } {G : Type u_6} [Group G] (h : (Nat.card G).Coprime n) {g : G} :
                                                        theorem Nat.Coprime.nsmul_right_bijective {G : Type u_1} [AddGroup G] {n : } (hn : (Nat.card G).Coprime n) :
                                                        Function.Bijective fun (x : G) => n x
                                                        theorem Nat.Coprime.pow_left_bijective {G : Type u_1} [Group G] {n : } (hn : (Nat.card G).Coprime n) :
                                                        Function.Bijective fun (x : G) => x ^ n
                                                        theorem add_inf_eq_bot_of_coprime {G : Type u_6} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} (h : (Nat.card H).Coprime (Nat.card K)) :
                                                        H K =
                                                        theorem inf_eq_bot_of_coprime {G : Type u_6} [Group G] {H : Subgroup G} {K : Subgroup G} (h : (Nat.card H).Coprime (Nat.card K)) :
                                                        H K =
                                                        theorem image_range_addOrderOf {G : Type u_1} [AddGroup G] [Fintype G] {x : G} [DecidableEq G] :
                                                        Finset.image (fun (i : ) => i x) (Finset.range (addOrderOf x)) = ((AddSubgroup.zmultiples x)).toFinset
                                                        theorem image_range_orderOf {G : Type u_1} [Group G] [Fintype G] {x : G} [DecidableEq G] :
                                                        Finset.image (fun (i : ) => x ^ i) (Finset.range (orderOf x)) = ((Subgroup.zpowers x)).toFinset
                                                        abbrev gcd_nsmul_card_eq_zero_iff.match_1 {G : Type u_1} [Fintype G] {n : } (motive : n.gcd (Fintype.card G) nProp) :
                                                        ∀ (x : n.gcd (Fintype.card G) n), (∀ (m : ) (hm : n = n.gcd (Fintype.card G) * m), motive )motive x
                                                        Equations
                                                        • =
                                                        Instances For
                                                          theorem gcd_nsmul_card_eq_zero_iff {G : Type u_1} [AddGroup G] [Fintype G] {x : G} {n : } :
                                                          n x = 0 n.gcd (Fintype.card G) x = 0
                                                          theorem pow_gcd_card_eq_one_iff {G : Type u_1} [Group G] [Fintype G] {x : G} {n : } :
                                                          x ^ n = 1 x ^ n.gcd (Fintype.card G) = 1
                                                          def addSubmonoidOfIdempotent {M : Type u_6} [AddLeftCancelMonoid M] [Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S + S = S) :

                                                          A nonempty idempotent subset of a finite cancellative add monoid is a submonoid

                                                          Equations
                                                          Instances For
                                                            theorem addSubmonoidOfIdempotent.proof_2 {M : Type u_1} [AddLeftCancelMonoid M] (S : Set M) (hS2 : S + S = S) :
                                                            ∀ {a b : M}, a Sb Sa + b S
                                                            theorem addSubmonoidOfIdempotent.proof_3 {M : Type u_1} [AddLeftCancelMonoid M] [Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S + S = S) (pow_mem : aS, ∀ (n : ), (n + 1) a S) :
                                                            0 { carrier := S, add_mem' := }.carrier
                                                            theorem addSubmonoidOfIdempotent.proof_1 {M : Type u_1} [AddLeftCancelMonoid M] (S : Set M) (hS2 : S + S = S) (a : M) (ha : a S) (t : ) :
                                                            (t + 1) a S
                                                            def submonoidOfIdempotent {M : Type u_6} [LeftCancelMonoid M] [Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S * S = S) :

                                                            A nonempty idempotent subset of a finite cancellative monoid is a submonoid

                                                            Equations
                                                            Instances For
                                                              theorem addSubgroupOfIdempotent.proof_3 {G : Type u_1} [AddGroup G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S + S = S) {a : G} (ha : a { carrier := S, add_mem' := , zero_mem' := }.carrier) :
                                                              theorem addSubgroupOfIdempotent.proof_1 {G : Type u_1} [AddGroup G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S + S = S) :
                                                              ∀ {a b : G}, a (addSubmonoidOfIdempotent S hS1 hS2).carrierb (addSubmonoidOfIdempotent S hS1 hS2).carriera + b (addSubmonoidOfIdempotent S hS1 hS2).carrier
                                                              def addSubgroupOfIdempotent {G : Type u_6} [AddGroup G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S + S = S) :

                                                              A nonempty idempotent subset of a finite add group is a subgroup

                                                              Equations
                                                              Instances For
                                                                theorem addSubgroupOfIdempotent.proof_2 {G : Type u_1} [AddGroup G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S + S = S) :
                                                                0 (addSubmonoidOfIdempotent S hS1 hS2).carrier
                                                                def subgroupOfIdempotent {G : Type u_6} [Group G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S * S = S) :

                                                                A nonempty idempotent subset of a finite group is a subgroup

                                                                Equations
                                                                Instances For
                                                                  theorem smulCardAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (one_mem : 0 Fintype.card G S) :
                                                                  ∃ (x : G), x Fintype.card G S
                                                                  theorem smulCardAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (one_mem : 0 Fintype.card G S) :
                                                                  def smulCardAddSubgroup {G : Type u_6} [AddGroup G] [Fintype G] (S : Set G) (hS : S.Nonempty) :

                                                                  If S is a nonempty subset of a finite add group G, then |G| • S is a subgroup

                                                                  Equations
                                                                  Instances For
                                                                    theorem smulCardAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (hS : S.Nonempty) :
                                                                    @[simp]
                                                                    theorem smulCardAddSubgroup_coe {G : Type u_6} [AddGroup G] [Fintype G] (S : Set G) (hS : S.Nonempty) :
                                                                    @[simp]
                                                                    theorem powCardSubgroup_coe {G : Type u_6} [Group G] [Fintype G] (S : Set G) (hS : S.Nonempty) :
                                                                    def powCardSubgroup {G : Type u_6} [Group G] [Fintype G] (S : Set G) (hS : S.Nonempty) :

                                                                    If S is a nonempty subset of a finite group G, then S ^ |G| is a subgroup

                                                                    Equations
                                                                    Instances For
                                                                      theorem IsOfFinOrder.eq_one {G : Type u_1} [LinearOrderedSemiring G] {a : G} (ha₀ : 0 a) (ha : IsOfFinOrder a) :
                                                                      a = 1
                                                                      theorem IsOfFinOrder.eq_neg_one {G : Type u_1} [LinearOrderedRing G] {a : G} (ha₀ : a 0) (ha : IsOfFinOrder a) :
                                                                      a = -1
                                                                      theorem orderOf_abs_ne_one {G : Type u_1} [LinearOrderedRing G] {x : G} (h : |x| 1) :
                                                                      theorem Prod.addOrderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] (x : α × β) :
                                                                      addOrderOf x = (addOrderOf x.1).lcm (addOrderOf x.2)
                                                                      theorem Prod.orderOf {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] (x : α × β) :
                                                                      orderOf x = (orderOf x.1).lcm (orderOf x.2)
                                                                      @[deprecated Prod.addOrderOf]
                                                                      theorem Prod.add_orderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] (x : α × β) :
                                                                      addOrderOf x = (addOrderOf x.1).lcm (addOrderOf x.2)

                                                                      Alias of Prod.addOrderOf.

                                                                      theorem addOrderOf_fst_dvd_addOrderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} :
                                                                      theorem orderOf_fst_dvd_orderOf {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} :
                                                                      @[deprecated addOrderOf_fst_dvd_addOrderOf]
                                                                      theorem add_orderOf_fst_dvd_add_orderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} :

                                                                      Alias of addOrderOf_fst_dvd_addOrderOf.

                                                                      theorem addOrderOf_snd_dvd_addOrderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} :
                                                                      theorem orderOf_snd_dvd_orderOf {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} :
                                                                      @[deprecated addOrderOf_snd_dvd_addOrderOf]
                                                                      theorem add_orderOf_snd_dvd_add_orderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} :

                                                                      Alias of addOrderOf_snd_dvd_addOrderOf.

                                                                      theorem IsOfFinAddOrder.fst {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} (hx : IsOfFinAddOrder x) :
                                                                      theorem IsOfFinOrder.fst {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} (hx : IsOfFinOrder x) :
                                                                      theorem IsOfFinAddOrder.snd {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} (hx : IsOfFinAddOrder x) :
                                                                      theorem IsOfFinOrder.snd {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} (hx : IsOfFinOrder x) :
                                                                      theorem IsOfFinAddOrder.prod_mk {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {a : α} {b : β} :
                                                                      theorem IsOfFinOrder.prod_mk {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {a : α} {b : β} :
                                                                      theorem Prod.addOrderOf_mk {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {a : α} {b : β} :
                                                                      addOrderOf (a, b) = (addOrderOf a).lcm (addOrderOf b)
                                                                      theorem Prod.orderOf_mk {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {a : α} {b : β} :
                                                                      orderOf (a, b) = (orderOf a).lcm (orderOf b)
                                                                      @[simp]
                                                                      theorem Nat.cast_card_eq_zero (R : Type u_6) [AddGroupWithOne R] [Fintype R] :
                                                                      (Fintype.card R) = 0
                                                                      theorem charP_of_ne_zero {R : Type u_6} [NonAssocRing R] [Fintype R] (p : ) (hn : Fintype.card R = p) (hR : i < p, i = 0i = 0) :
                                                                      CharP R p
                                                                      theorem charP_of_prime_pow_injective (R : Type u_6) [Ring R] [Fintype R] (p : ) (n : ) [hp : Fact (Nat.Prime p)] (hn : Fintype.card R = p ^ n) (hR : in, p ^ i = 0i = n) :
                                                                      CharP R (p ^ n)
                                                                      theorem AddSemiconjBy.addOrderOf_eq {G : Type u_1} [AddGroup G] (a : G) {x : G} {y : G} (h : AddSemiconjBy a x y) :
                                                                      theorem SemiconjBy.orderOf_eq {G : Type u_1} [Group G] (a : G) {x : G} {y : G} (h : SemiconjBy a x y) :