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
      theorem isOfFinAddOrder_iff_zsmul_eq_zero {G : Type u_6} [AddGroup G] {x : G} :
      IsOfFinAddOrder x ∃ (n : ), n 0 n x = 0
      theorem isOfFinOrder_iff_zpow_eq_one {G : Type u_6} [Group G] {x : G} :
      IsOfFinOrder x ∃ (n : ), n 0 x ^ n = 1
      @[simp]

      0 is of finite order in any additive monoid.

      @[simp]
      theorem IsOfFinOrder.one {G : Type u_1} [Monoid G] :

      1 is of finite order in any monoid.

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

      Alias of IsOfFinOrder.one.


      1 is of finite order in any monoid.

      @[deprecated]
      theorem IsOfFinAddOrder.nsmul {G : Type u_1} [AddMonoid G] {a : G} {n : } :
      theorem IsOfFinOrder.pow {G : Type u_1} [Monoid G] {a : G} {n : } :
      theorem IsOfFinAddOrder.of_nsmul {G : Type u_1} [AddMonoid G] {a : G} {n : } (h : IsOfFinAddOrder (n a)) (hn : n 0) :
      theorem IsOfFinOrder.of_pow {G : Type u_1} [Monoid G] {a : G} {n : } (h : IsOfFinOrder (a ^ n)) (hn : n 0) :
      @[simp]
      theorem isOfFinAddOrder_nsmul {G : Type u_1} [AddMonoid G] {a : G} {n : } :
      @[simp]
      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.

      @[reducible, inline]
      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
        @[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_unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) :
              hx.unit = x
              @[simp]
              theorem IsOfFinOrder.val_inv_unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) :
              hx.unit⁻¹ = x ^ (orderOf x - 1)
              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)
                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
                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
                  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.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 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 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
                    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.

                        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 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} :
                            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] {x : G} {y : G} [Finite 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] {x : G} {y : G} [Finite G] [DecidableEq G] :
                            y Subgroup.zpowers x y Finset.image (fun (x_1 : ) => x ^ x_1) (Finset.range (orderOf x))
                            noncomputable def zmultiplesEquivZMultiples {G : Type u_1} [AddGroup G] {x : G} {y : G} [Finite 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] {x : G} {y : G} [Finite 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] {x : G} {y : G} [Finite G] (h : addOrderOf x = addOrderOf y) (n : ) :
                                (zmultiplesEquivZMultiples h) n x, = n y,
                                @[simp]
                                theorem zpowersEquivZPowers_apply {G : Type u_1} [Group G] {x : G} {y : G} [Finite 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_6} [AddGroup G] (s : AddSubgroup G) {x : G} (hx : x s) :
                                theorem Subgroup.orderOf_dvd_natCard {G : Type u_6} [Group G] (s : Subgroup G) {x : G} (hx : x s) :
                                theorem AddSubgroup.addOrderOf_le_card {G : Type u_6} [AddGroup G] (s : AddSubgroup G) (hs : (↑s).Finite) {x : G} (hx : x s) :
                                theorem Subgroup.orderOf_le_card {G : Type u_6} [Group G] (s : Subgroup G) (hs : (↑s).Finite) {x : G} (hx : x s) :
                                theorem AddSubmonoid.addOrderOf_le_card {G : Type u_6} [AddGroup G] (s : AddSubmonoid G) (hs : (↑s).Finite) {x : G} (hx : x s) :
                                theorem Submonoid.orderOf_le_card {G : Type u_6} [Group G] (s : Submonoid G) (hs : (↑s).Finite) {x : G} (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_6} [AddGroup G] (a : G) (n : ) :
                                (n % Nat.card G) a = n a
                                @[simp]
                                theorem pow_mod_natCard {G : Type u_6} [Group G] (a : G) (n : ) :
                                a ^ (n % Nat.card G) = a ^ n
                                @[simp]
                                theorem mod_natCard_zsmul {G : Type u_6} [AddGroup G] (a : G) (n : ) :
                                (n % (Nat.card G)) a = n a
                                @[simp]
                                theorem zpow_mod_natCard {G : Type u_6} [Group G] (a : G) (n : ) :
                                a ^ (n % (Nat.card G)) = a ^ n
                                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
                                  @[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 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 nsmulCoprime_apply {n : } {G : Type u_6} [AddGroup G] (h : (Nat.card G).Coprime n) (g : G) :
                                  (nsmulCoprime h) g = n g
                                  @[simp]
                                  theorem powCoprime_apply {n : } {G : Type u_6} [Group G] (h : (Nat.card G).Coprime n) (g : G) :
                                  (powCoprime h) g = g ^ n
                                  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 {n : } {G : Type u_6} [AddGroup G] (hn : (Nat.card G).Coprime n) :
                                    Function.Bijective fun (x : G) => n x
                                    theorem Nat.Coprime.pow_left_bijective {n : } {G : Type u_6} [Group G] (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
                                    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
                                      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
                                        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
                                          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
                                            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
                                              @[simp]
                                              theorem powCardSubgroup_coe {G : Type u_6} [Group 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) :
                                              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] (p : ) [Fintype R] (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) :