# 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 #

• IsOfFinOrder is a predicate on an element x of a monoid G saying that x is of finite order.
• IsOfFinAddOrder is the additive analogue of IsOfFinOrder.
• orderOf x defines the order of an element x of a monoid G, by convention its value is 0 if x has infinite order.
• addOrderOf is the additive analogue of orderOf.

## Tags #

order of an element

theorem isPeriodicPt_add_iff_nsmul_eq_zero {G : Type u_1} [] {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} [] {n : } (x : G) :
Function.IsPeriodicPt (fun (x_1 : G) => x * x_1) n 1 x ^ n = 1
def IsOfFinAddOrder {G : Type u_1} [] (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} [] (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} [] {x : G} :
theorem isOfFinOrder_ofAdd_iff {α : Type u_6} [] {x : α} :
theorem isOfFinAddOrder_iff_nsmul_eq_zero {G : Type u_1} [] {x : G} :
∃ (n : ), 0 < n n x = 0
theorem isOfFinOrder_iff_pow_eq_one {G : Type u_1} [] {x : G} :
∃ (n : ), 0 < n x ^ n = 1
theorem IsOfFinOrder.exists_pow_eq_one {G : Type u_1} [] {x : G} :
∃ (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} [] {x : G} :
∃ (n : ), 0 < n n x = 0
abbrev isOfFinAddOrder_iff_zsmul_eq_zero.match_1 {G : Type u_1} [] {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} [] {x : G} :
∃ (n : ), n 0 n x = 0
abbrev isOfFinAddOrder_iff_zsmul_eq_zero.match_2 {G : Type u_1} [] {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} [] {x : G} :
∃ (n : ), n 0 x ^ n = 1
theorem not_isOfFinAddOrder_of_injective_nsmul {G : Type u_1} [] {x : G} (h : Function.Injective fun (n : ) => n x) :

See also injective_nsmul_iff_not_isOfFinAddOrder.

theorem not_isOfFinOrder_of_injective_pow {G : Type u_1} [] {x : G} (h : Function.Injective fun (n : ) => x ^ n) :

See also injective_pow_iff_not_isOfFinOrder.

theorem IsOfFinOrder.pow {G : Type u_1} [] {a : G} {n : } :
IsOfFinOrder (a ^ n)
theorem AddSubmonoid.isOfFinAddOrder_coe {G : Type u_1} [] {H : } {x : H} :

Elements of finite order are of finite order in submonoids.

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

Elements of finite order are of finite order in submonoids.

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

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

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

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 : ) (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 : ) (i : η) :

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

theorem isOfFinAddOrder_zero {G : Type u_1} [] :

0 is of finite order in any additive monoid.

theorem isOfFinOrder_one {G : Type u_1} [] :

1 is of finite order in any monoid.

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

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} [] {x : G} (hx : ) :
0 < .choose .choose x = 0
@[reducible, inline]
noncomputable abbrev IsOfFinOrder.groupPowers {G : Type u_1} [] {x : G} (hx : ) :

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} [] (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} [] (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} [] (x : G) :
@[simp]
theorem IsOfFinAddOrder.addOrderOf_pos {G : Type u_1} [] {x : G} (h : ) :
0 <
theorem IsOfFinOrder.orderOf_pos {G : Type u_1} [] {x : G} (h : ) :
0 <
theorem addOrderOf_nsmul_eq_zero {G : Type u_1} [] (x : G) :
x = 0
theorem pow_orderOf_eq_one {G : Type u_1} [] (x : G) :
x ^ = 1
theorem addOrderOf_eq_zero {G : Type u_1} [] {x : G} (h : ) :
= 0
theorem orderOf_eq_zero {G : Type u_1} [] {x : G} (h : ) :
= 0
theorem addOrderOf_eq_zero_iff {G : Type u_1} [] {x : G} :
= 0
theorem orderOf_eq_zero_iff {G : Type u_1} [] {x : G} :
= 0
theorem addOrderOf_eq_zero_iff' {G : Type u_1} [] {x : G} :
= 0 ∀ (n : ), 0 < nn x 0
theorem orderOf_eq_zero_iff' {G : Type u_1} [] {x : G} :
= 0 ∀ (n : ), 0 < nx ^ n 1
theorem addOrderOf_eq_iff {G : Type u_1} [] {x : G} {n : } (h : 0 < n) :
= n n x = 0 m < n, 0 < mm x 0
theorem orderOf_eq_iff {G : Type u_1} [] {x : G} {n : } (h : 0 < n) :
= n x ^ n = 1 m < n, 0 < mx ^ m 1
theorem addOrderOf_pos_iff {G : Type u_1} [] {x : G} :
0 <

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

theorem orderOf_pos_iff {G : Type u_1} [] {x : G} :
0 <

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

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

Alias of pow_ne_one_of_lt_orderOf.

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

Alias of nsmul_ne_zero_of_lt_addOrderOf.

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

Alias of IsOfFinAddOrder.multiples_eq_image_range_addOrderOf.

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

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} [] {x : G} {n : } (hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ (p : ), p nx ^ (n / p) 1) :
= n

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} [] {x : G} {H : Type u_6} [] {y : H} :
∀ (n : ), n x = 0 n y = 0
theorem orderOf_eq_orderOf_iff {G : Type u_1} [] {x : G} {H : Type u_6} [] {y : H} :
= ∀ (n : ), x ^ n = 1 y ^ n = 1
theorem addOrderOf_injective {G : Type u_1} [] {H : Type u_6} [] (f : G →+ H) (hf : ) (x : G) :

An injective homomorphism of additive monoids preserves orders of elements.

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

An injective homomorphism of monoids preserves orders of elements.

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

An additive equivalence preserves orders of elements.

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

A multiplicative equivalence preserves orders of elements.

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

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 ^ ( - 1), val_inv := , inv_val := }
Instances For
theorem IsOfFinOrder.isUnit {M : Type u_6} [] {x : M} (hx : ) :
theorem addOrderOf_nsmul' {G : Type u_1} [] (x : G) {n : } (h : n 0) :
addOrderOf (n x) = / ().gcd n
theorem orderOf_pow' {G : Type u_1} [] (x : G) {n : } (h : n 0) :
orderOf (x ^ n) = / ().gcd n
theorem addOrderOf_nsmul_of_dvd {G : Type u_1} [] {x : G} {n : } (hn : n 0) (dvd : n ) :
addOrderOf (n x) = / n
theorem orderOf_pow_of_dvd {G : Type u_1} [] {x : G} {n : } (hn : n 0) (dvd : n ) :
orderOf (x ^ n) = / n
theorem addOrderOf_nsmul_addOrderOf_sub {G : Type u_1} [] {x : G} {n : } (hx : 0) (hn : n ) :
addOrderOf (( / n) x) = n
theorem orderOf_pow_orderOf_div {G : Type u_1} [] {x : G} {n : } (hx : 0) (hn : n ) :
orderOf (x ^ ( / n)) = n
theorem IsOfFinAddOrder.addOrderOf_nsmul {G : Type u_1} [] (x : G) (n : ) (h : ) :
addOrderOf (n x) = / ().gcd n
theorem IsOfFinOrder.orderOf_pow {G : Type u_1} [] (x : G) (n : ) (h : ) :
orderOf (x ^ n) = / ().gcd n
theorem Nat.Coprime.addOrderOf_nsmul {G : Type u_1} [] {y : G} {m : } (h : ().Coprime m) :
theorem Nat.Coprime.orderOf_pow {G : Type u_1} [] {y : G} {m : } (h : ().Coprime m) :
orderOf (y ^ m) =
theorem IsOfFinAddOrder.natCard_multiples_le_addOrderOf {G : Type u_1} [] {a : G} (ha : ) :
theorem IsOfFinOrder.natCard_powers_le_orderOf {G : Type u_1} [] {a : G} (ha : ) :
Nat.card ()
theorem IsOfFinAddOrder.finite_multiples {G : Type u_1} [] {a : G} (ha : ) :
().Finite
theorem IsOfFinOrder.finite_powers {G : Type u_1} [] {a : G} (ha : ) :
(()).Finite
theorem AddCommute.addOrderOf_add_dvd_lcm {G : Type u_1} [] {x : G} {y : G} (h : ) :
addOrderOf (x + y) ().lcm ()
theorem Commute.orderOf_mul_dvd_lcm {G : Type u_1} [] {x : G} {y : G} (h : Commute x y) :
orderOf (x * y) ().lcm ()
theorem AddCommute.addOrderOf_dvd_lcm_add {G : Type u_1} [] {x : G} {y : G} (h : ) :
theorem Commute.orderOf_dvd_lcm_mul {G : Type u_1} [] {x : G} {y : G} (h : Commute x y) :
().lcm (orderOf (x * y))
theorem Commute.orderOf_mul_dvd_mul_orderOf {G : Type u_1} [] {x : G} {y : G} (h : Commute x y) :
orderOf (x * y) *
theorem Commute.orderOf_mul_eq_mul_orderOf_of_coprime {G : Type u_1} [] {x : G} {y : G} (h : Commute x y) (hco : ().Coprime ()) :
orderOf (x * y) = *
theorem AddCommute.isOfFinAddOrder_add {G : Type u_1} [] {x : G} {y : G} (h : ) (hx : ) (hy : ) :

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

Commuting elements of finite order are closed under multiplication.

theorem AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [] {x : G} {y : G} (h : ) (hy : ) (hdvd : ∀ (p : ), p p * ) :

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} [] {x : G} {y : G} (h : Commute x y) (hy : ) (hdvd : ∀ (p : ), p p * ) :
orderOf (x * 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} [] {x : G} {p : } [hp : Fact ()] (hg : p x = 0) (hg1 : x 0) :
= p
theorem orderOf_eq_prime {G : Type u_1} [] {x : G} {p : } [hp : Fact ()] (hg : x ^ p = 1) (hg1 : x 1) :
= p
theorem addOrderOf_eq_prime_pow {G : Type u_1} [] {x : G} {n : } {p : } [hp : Fact ()] (hnot : ¬p ^ n x = 0) (hfin : p ^ (n + 1) x = 0) :
= p ^ (n + 1)
theorem orderOf_eq_prime_pow {G : Type u_1} [] {x : G} {n : } {p : } [hp : Fact ()] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :
= p ^ (n + 1)
abbrev exists_addOrderOf_eq_prime_pow_iff.match_2 {G : Type u_1} [] {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} [] {x : G} {p : } (motive : (∃ (k : ), = p ^ k)Prop) :
∀ (x_1 : ∃ (k : ), = p ^ k), (∀ (k : ) (hk : = p ^ k), motive )motive x_1
Equations
• =
Instances For
theorem exists_addOrderOf_eq_prime_pow_iff {G : Type u_1} [] {x : G} {p : } [hp : Fact ()] :
(∃ (k : ), = p ^ k) ∃ (m : ), p ^ m x = 0
theorem exists_orderOf_eq_prime_pow_iff {G : Type u_1} [] {x : G} {p : } [hp : Fact ()] :
(∃ (k : ), = p ^ k) ∃ (m : ), x ^ p ^ m = 1
theorem nsmul_eq_nsmul_iff_modEq {G : Type u_1} {x : G} {m : } {n : } :
n x = m x n m [MOD ]
theorem pow_eq_pow_iff_modEq {G : Type u_1} [] {x : G} {m : } {n : } :
x ^ n = x ^ m n m [MOD ]
@[simp]
theorem injective_nsmul_iff_not_isOfFinAddOrder {G : Type u_1} {x : G} :
(Function.Injective fun (n : ) => n x)
@[simp]
theorem injective_pow_iff_not_isOfFinOrder {G : Type u_1} [] {x : G} :
(Function.Injective fun (n : ) => x ^ n)
theorem nsmul_inj_mod {G : Type u_1} {x : G} {n : } {m : } :
n x = m x n % = m %
theorem pow_inj_mod {G : Type u_1} [] {x : G} {n : } {m : } :
x ^ n = x ^ m n % = m %
theorem nsmul_inj_iff_of_addOrderOf_eq_zero {G : Type u_1} {x : G} (h : = 0) {n : } {m : } :
n x = m x n = m
theorem pow_inj_iff_of_orderOf_eq_zero {G : Type u_1} [] {x : G} (h : = 0) {n : } {m : } :
x ^ n = x ^ m n = m
theorem infinite_not_isOfFinAddOrder {G : Type u_1} {x : G} (h : ) :
{y : G | }.Infinite
theorem infinite_not_isOfFinOrder {G : Type u_1} [] {x : G} (h : ) :
{y : G | }.Infinite
@[simp]
theorem finite_multiples {G : Type u_1} {a : G} :
().Finite
@[simp]
theorem finite_powers {G : Type u_1} [] {a : G} :
(()).Finite
@[simp]
theorem infinite_multiples {G : Type u_1} {a : G} :
().Infinite
@[simp]
theorem infinite_powers {G : Type u_1} [] {a : G} :
(()).Infinite
abbrev finEquivMultiples.match_3 {G : Type u_1} (x : G) (motive : ) :
∀ (x_1 : ), (∀ (i : ), motive (fun (x_2 : ) => x_2 x) i, )motive x_1
Equations
• =
Instances For
abbrev finEquivMultiples.match_1 {G : Type u_1} (x : G) :
∀ (val : ) (h₁ : val < ) (motive : (x_1 : Fin ()) → (fun (n : Fin ()) => n x, ) val, h₁ = (fun (n : Fin ()) => n x, ) x_1Prop) (x_1 : Fin ()) (ij : (fun (n : Fin ()) => n x, ) val, h₁ = (fun (n : Fin ()) => n x, ) x_1), (∀ (val_1 : ) (h₂ : val_1 < ) (ij : (fun (n : Fin ()) => n x, ) val, h₁ = (fun (n : Fin ()) => n x, ) val_1, h₂), motive val_1, h₂ ij)motive x_1 ij
Equations
• =
Instances For
noncomputable def finEquivMultiples {G : Type u_1} (x : G) (hx : ) :
Fin ()

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} (x : G) (hx : ) :
(Function.Injective fun (n : Fin ()) => n x, ) Function.Surjective fun (n : Fin ()) => n x,
theorem finEquivMultiples.proof_1 {G : Type u_1} (x : G) (n : Fin ()) :
∃ (y : ), (fun (x_1 : ) => x_1 x) y = n x
abbrev finEquivMultiples.match_2 {G : Type u_1} (x : G) :
∀ (x_1 : Fin ()) (motive : (x_2 : Fin ()) → (fun (n : Fin ()) => n x, ) x_2 = (fun (n : Fin ()) => n x, ) x_1Prop) (x_2 : Fin ()) (ij : (fun (n : Fin ()) => n x, ) x_2 = (fun (n : Fin ()) => n x, ) x_1), (∀ (val : ) (h₁ : val < ) (ij : (fun (n : Fin ()) => n x, ) val, h₁ = (fun (n : Fin ()) => n x, ) x_1), motive val, h₁ ij)motive x_2 ij
Equations
• =
Instances For
noncomputable def finEquivPowers {G : Type u_1} [] (x : G) (hx : ) :
Fin () ()

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} (x : G) (hx : ) {n : Fin ()} :
() n = n x,
@[simp]
theorem finEquivPowers_apply {G : Type u_1} [] (x : G) (hx : ) {n : Fin ()} :
() n = x ^ n,
@[simp]
theorem finEquivMultiples_symm_apply {G : Type u_1} (x : G) (hx : ) (n : ) {hn : ∃ (m : ), m x = n x} :
().symm n x, hn = n % ,
@[simp]
theorem finEquivPowers_symm_apply {G : Type u_1} [] (x : G) (hx : ) (n : ) {hn : ∃ (m : ), x ^ m = x ^ n} :
().symm x ^ n, hn = n % ,
theorem Nat.card_addSubmonoidMultiples {G : Type u_1} {a : G} :

See also addOrder_eq_card_multiples.

theorem Nat.card_submonoidPowers {G : Type u_1} [] {a : G} :
=

See also orderOf_eq_card_powers.

@[simp]
theorem isOfFinAddOrder_neg_iff {G : Type u_1} [] {x : G} :

@[simp]
theorem isOfFinOrder_inv_iff {G : Type u_1} [] {x : G} :

Inverses of elements of finite order have finite order.

theorem IsOfFinOrder.inv {G : Type u_1} [] {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} [] {x : G} :

Alias of the forward direction of isOfFinOrder_inv_iff.

Inverses of elements of finite order have finite order.

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

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

Equations
• = ().trans ()
Instances For
noncomputable def finEquivZPowers {G : Type u_1} [] (x : G) (hx : ) :
Fin () ()

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

Equations
• = ().trans ()
Instances For
@[simp]
theorem finEquivZMultiples_apply {G : Type u_1} [] {x : G} (hx : ) {n : Fin ()} :
() n = n x,
@[simp]
theorem finEquivZPowers_apply {G : Type u_1} [] {x : G} (hx : ) {n : Fin ()} :
() n = x ^ n,
@[simp]
theorem finEquivZMultiples_symm_apply {G : Type u_1} [] (x : G) (hx : ) (n : ) :
().symm n x, = n % ,
@[simp]
theorem finEquivZPowers_symm_apply {G : Type u_1} [] (x : G) (hx : ) (n : ) :
().symm x ^ n, = n % ,
theorem IsOfFinAddOrder.add {G : Type u_1} [] {x : G} {y : G} (hx : ) (hy : ) :

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

Elements of finite order are closed under multiplication.

abbrev sum_card_addOrderOf_eq_card_nsmul_eq_zero.match_1 {G : Type u_1} [] {n : } (x : G) (motive : nProp) :
∀ (x_1 : n), (∀ (m : ) (hm : n = * m), motive )motive x_1
Equations
• =
Instances For
theorem sum_card_addOrderOf_eq_card_nsmul_eq_zero {G : Type u_1} [] {n : } [] [] (hn : n 0) :
mFinset.filter (fun (x : ) => x n) (Finset.range n.succ), (Finset.filter (fun (x : G) => = 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} [] {n : } [] [] (hn : n 0) :
mFinset.filter (fun (x : ) => x n) (Finset.range n.succ), (Finset.filter (fun (x : G) => = m) Finset.univ).card = (Finset.filter (fun (x : G) => x ^ n = 1) Finset.univ).card
theorem addOrderOf_le_card_univ {G : Type u_1} [] {x : G} [] :
theorem orderOf_le_card_univ {G : Type u_1} [] {x : G} [] :
theorem isOfFinAddOrder_of_finite {G : Type u_1} [] (x : G) :
theorem isOfFinOrder_of_finite {G : Type u_1} [] [] (x : G) :
theorem addOrderOf_pos {G : Type u_1} [] (x : G) :
0 <

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} [] [] (x : G) :
0 <

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} [] {n : } (x : G) :
addOrderOf (n x) = / ().gcd n

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} [] [] {n : } (x : G) :
orderOf (x ^ n) = / ().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_multiples_iff_mem_range_addOrderOf {G : Type u_1} [] {x : G} {y : G} [] :
y Finset.image (fun (x_1 : ) => x_1 x) ()
theorem mem_powers_iff_mem_range_orderOf {G : Type u_1} [] [] {x : G} {y : G} [] :
y Finset.image (fun (x_1 : ) => x ^ x_1) ()
noncomputable def multiplesEquivMultiples {G : Type u_1} [] {x : G} {y : G} (h : ) :

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

Equations
• = ().symm.trans (().trans ())
Instances For
noncomputable def powersEquivPowers {G : Type u_1} [] [] {x : G} {y : G} (h : = ) :
() ()

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

Equations
• = ().symm.trans (().trans ())
Instances For
@[simp]
theorem multiplesEquivMultiples_apply {G : Type u_1} [] {x : G} {y : G} (h : ) (n : ) :
n x, = n y,
@[simp]
theorem powersEquivPowers_apply {G : Type u_1} [] [] {x : G} {y : G} (h : = ) (n : ) :
x ^ n, = y ^ n,
theorem addOrderOf_eq_card_multiples {G : Type u_1} [] {x : G} :
theorem orderOf_eq_card_powers {G : Type u_1} [] [] {x : G} :
=
theorem exists_zsmul_eq_zero {G : Type u_1} [] [] (x : G) :
∃ (i : ) (_ : i 0), i x = 0
theorem exists_zpow_eq_one {G : Type u_1} [] [] (x : G) :
∃ (i : ) (_ : i 0), x ^ i = 1
theorem mem_multiples_iff_mem_zmultiples {G : Type u_1} [] [] {x : G} {y : G} :
theorem mem_powers_iff_mem_zpowers {G : Type u_1} [] [] {x : G} {y : G} :
theorem multiples_eq_zmultiples {G : Type u_1} [] [] (x : G) :
theorem powers_eq_zpowers {G : Type u_1} [] [] (x : G) :
() = ()
theorem mem_zmultiples_iff_mem_range_addOrderOf {G : Type u_1} [] [] {x : G} {y : G} [] :
y Finset.image (fun (x_1 : ) => x_1 x) ()
theorem mem_zpowers_iff_mem_range_orderOf {G : Type u_1} [] [] {x : G} {y : G} [] :
y Finset.image (fun (x_1 : ) => x ^ x_1) ()
theorem zsmul_eq_zero_iff_modEq {G : Type u_1} [] {x : G} {n : } :
n x = 0 n 0 [ZMOD ()]
theorem zpow_eq_one_iff_modEq {G : Type u_1} [] {x : G} {n : } :
x ^ n = 1 n 0 [ZMOD ()]
theorem zsmul_eq_zsmul_iff_modEq {G : Type u_1} [] {x : G} {m : } {n : } :
m x = n x m n [ZMOD ()]
theorem zpow_eq_zpow_iff_modEq {G : Type u_1} [] {x : G} {m : } {n : } :
x ^ m = x ^ n m n [ZMOD ()]
@[simp]
theorem injective_zsmul_iff_not_isOfFinAddOrder {G : Type u_1} [] {x : G} :
(Function.Injective fun (n : ) => n x)
@[simp]
theorem injective_zpow_iff_not_isOfFinOrder {G : Type u_1} [] {x : G} :
(Function.Injective fun (n : ) => x ^ n)
theorem zmultiplesEquivZMultiples.proof_2 {G : Type u_1} [] [] {y : G} :
theorem zmultiplesEquivZMultiples.proof_1 {G : Type u_1} [] [] {x : G} :
noncomputable def zmultiplesEquivZMultiples {G : Type u_1} [] [] {x : G} {y : G} (h : ) :

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

Equations
• = ().symm.trans (().trans ())
Instances For
noncomputable def zpowersEquivZPowers {G : Type u_1} [] [] {x : G} {y : G} (h : = ) :
() ()

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

Equations
• = ().symm.trans (().trans ())
Instances For
@[simp]
theorem zmultiples_equiv_zmultiples_apply {G : Type u_1} [] [] {x : G} {y : G} (h : ) (n : ) :
n x, = n y,
@[simp]
theorem zpowersEquivZPowers_apply {G : Type u_1} [] [] {x : G} {y : G} (h : = ) (n : ) :
x ^ n, = y ^ n,
theorem Fintype.card_zmultiples {G : Type u_1} [] [] {x : G} :

See also Nat.card_subgroup.

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

See also Nat.card_addSubgroupZPowers.

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

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

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

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

Equations
• = { toFun := fun (g : G) => g ^ n, invFun := fun (g : G) => g ^ ().gcdB n, left_inv := , right_inv := }
Instances For
theorem nsmulCoprime_zero {n : } {G : Type u_6} [] (h : ().Coprime n) :
() 0 = 0
theorem powCoprime_one {n : } {G : Type u_6} [] (h : ().Coprime n) :
() 1 = 1
theorem nsmulCoprime_neg {n : } {G : Type u_6} [] (h : ().Coprime n) {g : G} :
() (-g) = -() g
theorem powCoprime_inv {n : } {G : Type u_6} [] (h : ().Coprime n) {g : G} :
() g⁻¹ = (() g)⁻¹
theorem Nat.Coprime.nsmul_right_bijective {G : Type u_1} [] {n : } (hn : ().Coprime n) :
Function.Bijective fun (x : G) => n x
theorem Nat.Coprime.pow_left_bijective {G : Type u_1} [] {n : } (hn : ().Coprime n) :
Function.Bijective fun (x : G) => x ^ n
theorem add_inf_eq_bot_of_coprime {G : Type u_6} [] {H : } {K : } (h : (Nat.card H).Coprime (Nat.card K)) :
H K =
theorem inf_eq_bot_of_coprime {G : Type u_6} [] {H : } {K : } (h : (Nat.card H).Coprime (Nat.card K)) :
H K =
theorem image_range_addOrderOf {G : Type u_1} [] [] {x : G} [] :
Finset.image (fun (i : ) => i x) () = ().toFinset
theorem image_range_orderOf {G : Type u_1} [] [] {x : G} [] :
Finset.image (fun (i : ) => x ^ i) () = (()).toFinset
abbrev gcd_nsmul_card_eq_zero_iff.match_1 {G : Type u_1} [] {n : } (motive : n.gcd () nProp) :
∀ (x : n.gcd () n), (∀ (m : ) (hm : n = n.gcd () * m), motive )motive x
Equations
• =
Instances For
theorem gcd_nsmul_card_eq_zero_iff {G : Type u_1} [] [] {x : G} {n : } :
n x = 0 n.gcd () x = 0
theorem pow_gcd_card_eq_one_iff {G : Type u_1} [] [] {x : G} {n : } :
x ^ n = 1 x ^ n.gcd () = 1
def addSubmonoidOfIdempotent {M : Type u_6} [] (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} (S : Set M) (hS2 : S + S = S) :
∀ {a b : M}, a Sb Sa + b S
theorem addSubmonoidOfIdempotent.proof_3 {M : Type u_1} [] (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} (S : Set M) (hS2 : S + S = S) (a : M) (ha : a S) (t : ) :
(t + 1) a S
def submonoidOfIdempotent {M : Type u_6} [] [] (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} [] [] (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} [] [] (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} [] [] (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} [] [] (S : Set G) (hS1 : S.Nonempty) (hS2 : S + S = S) :
def subgroupOfIdempotent {G : Type u_6} [] [] (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} [] [] (S : Set G) (one_mem : 0 ) :
∃ (x : G), x
theorem smulCardAddSubgroup.proof_3 {G : Type u_1} [] [] (S : Set G) (one_mem : 0 ) :
+ =
def smulCardAddSubgroup {G : Type u_6} [] [] (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} [] [] (S : Set G) (hS : S.Nonempty) :
0
@[simp]
theorem smulCardAddSubgroup_coe {G : Type u_6} [] [] (S : Set G) (hS : S.Nonempty) :
() =
@[simp]
theorem powCardSubgroup_coe {G : Type u_6} [] [] (S : Set G) (hS : S.Nonempty) :
() =
def powCardSubgroup {G : Type u_6} [] [] (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} {a : G} (ha₀ : 0 a) (ha : ) :
a = 1
theorem IsOfFinOrder.eq_neg_one {G : Type u_1} {a : G} (ha₀ : a 0) (ha : ) :
a = -1
theorem orderOf_abs_ne_one {G : Type u_1} {x : G} (h : |x| 1) :
= 0
theorem LinearOrderedRing.orderOf_le_two {G : Type u_1} {x : G} :
2
theorem Prod.addOrderOf {α : Type u_4} {β : Type u_5} [] [] (x : α × β) :
theorem Prod.orderOf {α : Type u_4} {β : Type u_5} [] [] (x : α × β) :
= (orderOf x.1).lcm (orderOf x.2)
theorem Prod.add_orderOf {α : Type u_4} {β : Type u_5} [] [] (x : α × β) :

Alias of Prod.addOrderOf.

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

Alias of addOrderOf_fst_dvd_addOrderOf.

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

Alias of addOrderOf_snd_dvd_addOrderOf.

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