# mathlib3documentation

group_theory.order_of_element

# Order of an element #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

• `is_of_fin_order` is a predicate on an element `x` of a monoid `G` saying that `x` is of finite order.
• `is_of_fin_add_order` is the additive analogue of `is_of_fin_order`.
• `order_of x` defines the order of an element `x` of a monoid `G`, by convention its value is `0` if `x` has infinite order.
• `add_order_of` is the additive analogue of `order_of`.

## Tags #

order of an element

theorem is_periodic_pt_add_iff_nsmul_eq_zero {G : Type u_1} [add_monoid G] {n : } (x : G) :
n x = 0
theorem is_periodic_pt_mul_iff_pow_eq_one {G : Type u_1} [monoid G] {n : } (x : G) :
x ^ n = 1
def is_of_fin_add_order {A : Type u_3} [add_monoid A] (a : A) :
Prop

`is_of_fin_add_order` 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
def is_of_fin_order {G : Type u_1} [monoid G] (x : G) :
Prop

`is_of_fin_order` 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
theorem is_of_fin_add_order_of_mul_iff {G : Type u_1} [monoid G] {x : G} :
theorem is_of_fin_order_of_add_iff {A : Type u_3} [add_monoid A] {a : A} :
theorem is_of_fin_order_iff_pow_eq_one {G : Type u_1} [monoid G] (x : G) :
(n : ), 0 < n x ^ n = 1
theorem is_of_fin_add_order_iff_nsmul_eq_zero {G : Type u_1} [add_monoid G] (x : G) :
(n : ), 0 < n n x = 0
theorem not_is_of_fin_order_of_injective_pow {G : Type u_1} [monoid G] {x : G} (h : function.injective (λ (n : ), x ^ n)) :

See also `injective_pow_iff_not_is_of_fin_order`.

theorem not_is_of_fin_add_order_of_injective_nsmul {G : Type u_1} [add_monoid G] {x : G} (h : function.injective (λ (n : ), n x)) :

See also `injective_nsmul_iff_not_is_of_fin_add_order`.

theorem is_of_fin_add_order_iff_coe {G : Type u_1} [add_monoid G] (H : add_submonoid G) (x : H) :

Elements of finite order are of finite order in submonoids.

theorem is_of_fin_order_iff_coe {G : Type u_1} [monoid G] (H : submonoid G) (x : H) :

Elements of finite order are of finite order in submonoids.

theorem add_monoid_hom.is_of_fin_order {G : Type u_1} {H : Type u_2} [add_monoid G] [add_monoid H] (f : G →+ H) {x : G} (h : is_of_fin_add_order x) :

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

theorem monoid_hom.is_of_fin_order {G : Type u_1} {H : Type u_2} [monoid G] [monoid H] (f : G →* H) {x : G} (h : is_of_fin_order x) :

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

theorem is_of_fin_order.apply {η : Type u_1} {Gs : η Type u_2} [Π (i : η), monoid (Gs i)] {x : Π (i : η), Gs i} (h : is_of_fin_order x) (i : η) :

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

theorem is_of_fin_add_order.apply {η : Type u_1} {Gs : η Type u_2} [Π (i : η), add_monoid (Gs i)] {x : Π (i : η), Gs i} (h : is_of_fin_add_order x) (i : η) :

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

theorem is_of_fin_order_zero {G : Type u_1} [add_monoid G] :

0 is of finite order in any additive monoid.

theorem is_of_fin_order_one {G : Type u_1} [monoid G] :

1 is of finite order in any monoid.

noncomputable def order_of {G : Type u_1} [monoid G] (x : G) :

`order_of 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 `order_of x` is `0` by convention.

Equations
noncomputable def add_order_of {G : Type u_1} [add_monoid G] (x : G) :

`add_order_of 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 `add_order_of a` is `0` by convention.

Equations
@[simp]
theorem add_order_of_of_mul_eq_order_of {G : Type u_1} [monoid G] (x : G) :
@[simp]
theorem order_of_of_add_eq_add_order_of {A : Type u_3} [add_monoid A] (a : A) :
theorem add_order_of_pos' {G : Type u_1} [add_monoid G] {x : G} (h : is_of_fin_add_order x) :
theorem order_of_pos' {G : Type u_1} [monoid G] {x : G} (h : is_of_fin_order x) :
0 <
theorem pow_order_of_eq_one {G : Type u_1} [monoid G] (x : G) :
x ^ = 1
theorem add_order_of_nsmul_eq_zero {G : Type u_1} [add_monoid G] (x : G) :
= 0
theorem order_of_eq_zero {G : Type u_1} [monoid G] {x : G} (h : ¬) :
= 0
theorem add_order_of_eq_zero {G : Type u_1} [add_monoid G] {x : G} (h : ¬) :
theorem add_order_of_eq_zero_iff {G : Type u_1} [add_monoid G] {x : G} :
theorem order_of_eq_zero_iff {G : Type u_1} [monoid G] {x : G} :
= 0
theorem order_of_eq_zero_iff' {G : Type u_1} [monoid G] {x : G} :
= 0 (n : ), 0 < n x ^ n 1
theorem add_order_of_eq_zero_iff' {G : Type u_1} [add_monoid G] {x : G} :
(n : ), 0 < n n x 0
theorem add_order_of_eq_iff {G : Type u_1} [add_monoid G] {x : G} {n : } (h : 0 < n) :
n x = 0 (m : ), m < n 0 < m m x 0
theorem order_of_eq_iff {G : Type u_1} [monoid G] {x : G} {n : } (h : 0 < n) :
= n x ^ n = 1 (m : ), m < n 0 < m x ^ m 1
theorem add_order_of_pos_iff {G : Type u_1} [add_monoid G] {x : G} :

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

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

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

theorem is_of_fin_add_order.mono {G : Type u_1} {β : Type u_5} [add_monoid G] {x : G} [add_monoid β] {y : β} (hx : is_of_fin_add_order x) (h : ) :
theorem is_of_fin_order.mono {G : Type u_1} {β : Type u_5} [monoid G] {x : G} [monoid β] {y : β} (hx : is_of_fin_order x) (h : ) :
theorem pow_ne_one_of_lt_order_of' {G : Type u_1} [monoid G] {x : G} {n : } (n0 : n 0) (h : n < ) :
x ^ n 1
theorem nsmul_ne_zero_of_lt_add_order_of' {G : Type u_1} [add_monoid G] {x : G} {n : } (n0 : n 0) (h : n < ) :
n x 0
theorem add_order_of_le_of_nsmul_eq_zero {G : Type u_1} [add_monoid G] {x : G} {n : } (hn : 0 < n) (h : n x = 0) :
theorem order_of_le_of_pow_eq_one {G : Type u_1} [monoid G] {x : G} {n : } (hn : 0 < n) (h : x ^ n = 1) :
n
@[simp]
theorem order_of_one {G : Type u_1} [monoid G] :
= 1
@[simp]
theorem order_of_zero {G : Type u_1} [add_monoid G] :
@[simp]
theorem order_of_eq_one_iff {G : Type u_1} [monoid G] {x : G} :
= 1 x = 1
@[simp]
theorem add_monoid.order_of_eq_one_iff {G : Type u_1} [add_monoid G] {x : G} :
x = 0
theorem pow_eq_mod_order_of {G : Type u_1} [monoid G] {x : G} {n : } :
x ^ n = x ^ (n % order_of x)
theorem nsmul_eq_mod_add_order_of {G : Type u_1} [add_monoid G] {x : G} {n : } :
n x = (n % x
theorem order_of_dvd_of_pow_eq_one {G : Type u_1} [monoid G] {x : G} {n : } (h : x ^ n = 1) :
n
theorem add_order_of_dvd_of_nsmul_eq_zero {G : Type u_1} [add_monoid G] {x : G} {n : } (h : n x = 0) :
theorem add_order_of_dvd_iff_nsmul_eq_zero {G : Type u_1} [add_monoid G] {x : G} {n : } :
n x = 0
theorem order_of_dvd_iff_pow_eq_one {G : Type u_1} [monoid G] {x : G} {n : } :
n x ^ n = 1
theorem add_order_of_smul_dvd {G : Type u_1} [add_monoid G] {x : G} (n : ) :
theorem order_of_pow_dvd {G : Type u_1} [monoid G] {x : G} (n : ) :
order_of (x ^ n)
theorem add_order_of_map_dvd {G : Type u_1} [add_monoid G] {H : Type u_2} [add_monoid H] (ψ : G →+ H) (x : G) :
theorem order_of_map_dvd {G : Type u_1} [monoid G] {H : Type u_2} [monoid H] (ψ : G →* H) (x : G) :
theorem exists_pow_eq_self_of_coprime {G : Type u_1} [monoid G] {x : G} {n : } (h : n.coprime (order_of x)) :
(m : ), (x ^ n) ^ m = x
theorem exists_nsmul_eq_self_of_coprime {G : Type u_1} [add_monoid G] {x : G} {n : } (h : n.coprime (add_order_of x)) :
(m : ), m n x = x
theorem add_order_of_eq_of_nsmul_and_div_prime_nsmul {G : Type u_1} [add_monoid G] {x : G} {n : } (hn : 0 < n) (hx : n x = 0) (hd : (p : ), p 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 order_of_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 : ), p n x ^ (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 order_of_eq_order_of_iff {G : Type u_1} [monoid G] {x : G} {H : Type u_2} [monoid H] {y : H} :
(n : ), x ^ n = 1 y ^ n = 1
theorem add_order_of_eq_add_order_of_iff {G : Type u_1} [add_monoid G] {x : G} {H : Type u_2} [add_monoid H] {y : H} :
(n : ), n x = 0 n y = 0
theorem order_of_injective {G : Type u_1} [monoid G] {H : Type u_2} [monoid H] (f : G →* H) (hf : function.injective f) (x : G) :
order_of (f x) =
theorem add_order_of_injective {G : Type u_1} [add_monoid G] {H : Type u_2} [add_monoid H] (f : G →+ H) (hf : function.injective f) (x : G) :
@[simp, norm_cast]
theorem order_of_submonoid {G : Type u_1} [monoid G] {H : submonoid G} (y : H) :
@[simp, norm_cast]
theorem order_of_add_submonoid {G : Type u_1} [add_monoid G] {H : add_submonoid G} (y : H) :
theorem order_of_units {G : Type u_1} [monoid G] {y : Gˣ} :
theorem order_of_add_units {G : Type u_1} [add_monoid G] {y : add_units G} :
theorem add_order_of_nsmul' {G : Type u_1} [add_monoid G] (x : G) {n : } (h : n 0) :
theorem order_of_pow' {G : Type u_1} [monoid G] (x : G) {n : } (h : n 0) :
order_of (x ^ n) = / (order_of x).gcd n
theorem add_order_of_nsmul'' {G : Type u_1} [add_monoid G] (x : G) (n : ) (h : is_of_fin_add_order x) :
theorem order_of_pow'' {G : Type u_1} [monoid G] (x : G) (n : ) (h : is_of_fin_order x) :
order_of (x ^ n) = / (order_of x).gcd n
theorem add_order_of_nsmul_coprime {G : Type u_1} [add_monoid G] {y : G} {m : } (h : (add_order_of y).coprime m) :
theorem order_of_pow_coprime {G : Type u_1} [monoid G] {y : G} {m : } (h : (order_of y).coprime m) :
order_of (y ^ m) =
theorem commute.order_of_mul_dvd_lcm {G : Type u_1} [monoid G] {x y : G} (h : y) :
theorem add_commute.order_of_add_dvd_lcm {G : Type u_1} [add_monoid G] {x y : G} (h : y) :
theorem commute.order_of_dvd_lcm_mul {G : Type u_1} [monoid G] {x y : G} (h : y) :
(order_of x).lcm (order_of (x * y))
theorem add_commute.order_of_dvd_lcm_add {G : Type u_1} [add_monoid G] {x y : G} (h : y) :
theorem commute.order_of_mul_dvd_mul_order_of {G : Type u_1} [monoid G] {x y : G} (h : y) :
order_of (x * y)
theorem add_commute.add_order_of_add_dvd_mul_add_order_of {G : Type u_1} [add_monoid G] {x y : G} (h : y) :
theorem commute.order_of_mul_eq_mul_order_of_of_coprime {G : Type u_1} [monoid G] {x y : G} (h : y) (hco : (order_of x).coprime (order_of y)) :
order_of (x * y) =
theorem add_commute.is_of_fin_order_add {G : Type u_1} [add_monoid G] {x y : G} (h : y) (hx : is_of_fin_add_order x) (hy : is_of_fin_add_order y) :

Commuting elements of finite additive order are closed under addition.

theorem commute.is_of_fin_order_mul {G : Type u_1} [monoid G] {x y : G} (h : y) (hx : is_of_fin_order x) (hy : is_of_fin_order y) :

Commuting elements of finite order are closed under multiplication.

theorem add_commute.add_order_of_add_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [add_monoid G] {x y : G} (h : y) (hy : is_of_fin_add_order y) (hdvd : (p : ), ) :

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

theorem commute.order_of_mul_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [monoid G] {x y : G} (h : y) (hy : is_of_fin_order y) (hdvd : (p : ), p p * ) :
order_of (x * y) =

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

theorem add_order_of_eq_prime {G : Type u_1} [add_monoid G] {x : G} {p : } [hp : fact (nat.prime p)] (hg : p x = 0) (hg1 : x 0) :
theorem order_of_eq_prime {G : Type u_1} [monoid G] {x : G} {p : } [hp : fact (nat.prime p)] (hg : x ^ p = 1) (hg1 : x 1) :
= p
theorem add_order_of_eq_prime_pow {G : Type u_1} [add_monoid G] {x : G} {n p : } [hp : fact (nat.prime p)] (hnot : ¬p ^ n x = 0) (hfin : p ^ (n + 1) x = 0) :
= p ^ (n + 1)
theorem order_of_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) :
= p ^ (n + 1)
theorem exists_add_order_of_eq_prime_pow_iff {G : Type u_1} [add_monoid G] {x : G} {p : } [hp : fact (nat.prime p)] :
( (k : ), = p ^ k) (m : ), p ^ m x = 0
theorem exists_order_of_eq_prime_pow_iff {G : Type u_1} [monoid G] {x : G} {p : } [hp : fact (nat.prime p)] :
( (k : ), = p ^ k) (m : ), x ^ p ^ m = 1
theorem nsmul_injective_of_lt_add_order_of {G : Type u_1} (x : G) {m n : } (hn : n < ) (hm : m < ) (eq : n x = m x) :
n = m
theorem pow_injective_of_lt_order_of {G : Type u_1} (x : G) {m n : } (hn : n < ) (hm : m < ) (eq : x ^ n = x ^ m) :
n = m
theorem mem_powers_iff_mem_range_order_of' {G : Type u_1} (x y : G) [decidable_eq G] (hx : 0 < ) :
theorem mem_multiples_iff_mem_range_add_order_of' {G : Type u_1} (x y : G) [decidable_eq G] (hx : 0 < ) :
y finset.image (λ (ᾰ : ), x) (finset.range (add_order_of x))
theorem pow_eq_one_iff_modeq {G : Type u_1} (x : G) {n : } :
x ^ n = 1 n 0 [MOD ]
theorem nsmul_eq_zero_iff_modeq {G : Type u_1} (x : G) {n : } :
n x = 0
theorem pow_eq_pow_iff_modeq {G : Type u_1} (x : G) {m n : } :
x ^ n = x ^ m n m [MOD ]
theorem nsmul_eq_nsmul_iff_modeq {G : Type u_1} (x : G) {m n : } :
n x = m x
@[simp]
theorem injective_pow_iff_not_is_of_fin_order {G : Type u_1} {x : G} :
function.injective (λ (n : ), x ^ n)
@[simp]
theorem injective_nsmul_iff_not_is_of_fin_add_order {G : Type u_1} {x : G} :
function.injective (λ (n : ), n x)
theorem infinite_not_is_of_fin_add_order {G : Type u_1} {x : G} (h : ¬) :
{y : G | .infinite
theorem infinite_not_is_of_fin_order {G : Type u_1} {x : G} (h : ¬) :
{y : G | .infinite
theorem is_of_fin_order.inv {G : Type u_1} [group G] {x : G} (hx : is_of_fin_order x) :

Inverses of elements of finite order have finite order.

theorem is_of_fin_add_order.neg {G : Type u_1} [add_group G] {x : G} (hx : is_of_fin_add_order x) :

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

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

Inverses of elements of finite order have finite order.

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

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

theorem order_of_dvd_iff_zpow_eq_one {G : Type u_1} [group G] {x : G} {i : } :
(order_of x) i x ^ i = 1
theorem add_order_of_dvd_iff_zsmul_eq_zero {G : Type u_1} [add_group G] {x : G} {i : } :
@[simp]
theorem order_of_neg {G : Type u_1} [add_group G] (x : G) :
@[simp]
theorem order_of_inv {G : Type u_1} [group G] (x : G) :
@[simp, norm_cast]
theorem order_of_add_subgroup {G : Type u_1} [add_group G] {H : add_subgroup G} (y : H) :
@[simp, norm_cast]
theorem order_of_subgroup {G : Type u_1} [group G] {H : subgroup G} (y : H) :
theorem zsmul_eq_mod_add_order_of {G : Type u_1} [add_group G] {x : G} {i : } :
i x = (i % (add_order_of x)) x
theorem zpow_eq_mod_order_of {G : Type u_1} [group G] {x : G} {i : } :
x ^ i = x ^ (i % (order_of x))
theorem pow_inj_iff_of_order_of_eq_zero {G : Type u_1} [group G] {x : G} (h : = 0) {n m : } :
x ^ n = x ^ m n = m
theorem nsmul_inj_iff_of_add_order_of_eq_zero {G : Type u_1} [add_group G] {x : G} (h : = 0) {n m : } :
n x = m x n = m
theorem nsmul_inj_mod {G : Type u_1} [add_group G] {x : G} {n m : } :
n x = m x =
theorem pow_inj_mod {G : Type u_1} [group G] {x : G} {n m : } :
x ^ n = x ^ m n % = m %
@[simp]
theorem zpow_pow_order_of {G : Type u_1} [group G] {x : G} {i : } :
(x ^ i) ^ = 1
@[simp]
theorem zsmul_smul_order_of {G : Type u_1} [add_group G] {x : G} {i : } :
i x = 0
theorem is_of_fin_add_order.zsmul {G : Type u_1} [add_group G] {x : G} (h : is_of_fin_add_order x) {i : } :
theorem is_of_fin_order.zpow {G : Type u_1} [group G] {x : G} (h : is_of_fin_order x) {i : } :
theorem is_of_fin_order.of_mem_zpowers {G : Type u_1} [group G] {x y : G} (h : is_of_fin_order x) (h' : y ) :
theorem is_of_fin_add_order.of_mem_zmultiples {G : Type u_1} [add_group G] {x y : G} (h : is_of_fin_add_order x) (h' : y ) :
theorem add_order_of_dvd_of_mem_zmultiples {G : Type u_1} [add_group G] {x y : G} (h : y ) :
theorem order_of_dvd_of_mem_zpowers {G : Type u_1} [group G] {x y : G} (h : y ) :
theorem smul_eq_self_of_mem_zpowers {G : Type u_1} [group G] {x y : G} {α : Type u_2} [ α] (hx : x ) {a : α} (hs : y a = a) :
x a = a
theorem vadd_eq_self_of_mem_zmultiples {α : Type u_1} {G : Type u_2} [add_group G] [ α] {x y : G} (hx : x ) {a : α} (hs : y +ᵥ a = a) :
x +ᵥ a = a
theorem is_of_fin_order.mul {G : Type u_1} [comm_monoid G] {x y : G} (hx : is_of_fin_order x) (hy : is_of_fin_order y) :

Elements of finite order are closed under multiplication.

theorem is_of_fin_add_order.add {G : Type u_1} {x y : G} (hx : is_of_fin_add_order x) (hy : is_of_fin_add_order y) :

Elements of finite additive order are closed under addition.

theorem sum_card_order_of_eq_card_pow_eq_one {G : Type u_1} [monoid G] {n : } [fintype G] [decidable_eq G] (hn : n 0) :
(finset.filter (λ (_x : ), _x n) (finset.range n.succ)).sum (λ (m : ), (finset.filter (λ (x : G), = m) finset.univ).card) = (finset.filter (λ (x : G), x ^ n = 1) finset.univ).card
theorem sum_card_add_order_of_eq_card_nsmul_eq_zero {G : Type u_1} [add_monoid G] {n : } [fintype G] [decidable_eq G] (hn : n 0) :
(finset.filter (λ (_x : ), _x n) (finset.range n.succ)).sum (λ (m : ), (finset.filter (λ (x : G), = m) finset.univ).card) = (finset.filter (λ (x : G), n x = 0) finset.univ).card
theorem exists_pow_eq_one {G : Type u_1} [finite G] (x : G) :
theorem exists_nsmul_eq_zero {G : Type u_1} [finite G] (x : G) :
theorem order_of_le_card_univ {G : Type u_1} {x : G} [fintype G] :
theorem add_order_of_le_card_univ {G : Type u_1} {x : G} [fintype G] :
theorem order_of_pos {G : Type u_1} [finite G] (x : G) :
0 <

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

theorem add_order_of_pos {G : Type u_1} [finite G] (x : G) :

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

theorem add_order_of_nsmul {G : Type u_1} {n : } [finite G] (x : G) :

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

theorem order_of_pow {G : Type u_1} {n : } [finite G] (x : G) :
order_of (x ^ n) = / (order_of x).gcd n

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

theorem mem_multiples_iff_mem_range_add_order_of {G : Type u_1} {x y : G} [finite G] [decidable_eq G] :
y finset.image (λ (ᾰ : ), x) (finset.range (add_order_of x))
@[protected, instance]
noncomputable def decidable_multiples {G : Type u_1} {x : G} :
Equations
@[protected, instance]
noncomputable def decidable_powers {G : Type u_1} {x : G} :
decidable_pred (λ (_x : G), _x submonoid.powers x)
Equations
noncomputable def fin_equiv_multiples {G : Type u_1} [finite G] (x : G) :

The equivalence between `fin (add_order_of a)` and `add_submonoid.multiples a`, sending `i` to `i • a`.

Equations
noncomputable def fin_equiv_powers {G : Type u_1} [finite G] (x : G) :

The equivalence between `fin (order_of x)` and `submonoid.powers x`, sending `i` to `x ^ i`."

Equations
@[simp]
theorem fin_equiv_multiples_apply {G : Type u_1} [finite G] {x : G} {n : fin (add_order_of x)} :
n = n x, _⟩
@[simp]
theorem fin_equiv_powers_apply {G : Type u_1} [finite G] {x : G} {n : fin (order_of x)} :
n = x ^ n, _⟩
@[simp]
theorem fin_equiv_multiples_symm_apply {G : Type u_1} [finite G] (x : G) (n : ) {hn : (m : ), m x = n x} :
.symm) n x, hn⟩ = , _⟩
@[simp]
theorem fin_equiv_powers_symm_apply {G : Type u_1} [finite G] (x : G) (n : ) {hn : (m : ), x ^ m = x ^ n} :
((fin_equiv_powers x).symm) x ^ n, hn⟩ = n % , _⟩
noncomputable def powers_equiv_powers {G : Type u_1} {x y : G} [finite G] (h : = ) :

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

Equations
noncomputable def multiples_equiv_multiples {G : Type u_1} {x y : G} [finite G] (h : = ) :

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

Equations
@[simp]
theorem powers_equiv_powers_apply {G : Type u_1} {x y : G} [finite G] (h : = ) (n : ) :
x ^ n, _⟩ = y ^ n, _⟩
@[simp]
theorem multiples_equiv_multiples_apply {G : Type u_1} {x y : G} [finite G] (h : = ) (n : ) :
n x, _⟩ = n y, _⟩
theorem add_order_of_eq_card_multiples {G : Type u_1} {x : G} [fintype G] :
theorem order_eq_card_powers {G : Type u_1} {x : G} [fintype G] :
theorem exists_zpow_eq_one {G : Type u_1} [group G] [finite G] (x : G) :
(i : ) (H : i 0), x ^ i = 1
theorem exists_zsmul_eq_zero {G : Type u_1} [add_group G] [finite G] (x : G) :
(i : ) (H : i 0), i x = 0
theorem mem_multiples_iff_mem_zmultiples {G : Type u_1} [add_group G] {x y : G} [finite G] :
theorem mem_powers_iff_mem_zpowers {G : Type u_1} [group G] {x y : G} [finite G] :
theorem multiples_eq_zmultiples {G : Type u_1} [add_group G] [finite G] (x : G) :
theorem powers_eq_zpowers {G : Type u_1} [group G] [finite G] (x : G) :
theorem mem_zmultiples_iff_mem_range_add_order_of {G : Type u_1} [add_group G] {x y : G} [finite G] [decidable_eq G] :
y finset.image (λ (ᾰ : ), x) (finset.range (add_order_of x))
theorem mem_zpowers_iff_mem_range_order_of {G : Type u_1} [group G] {x y : G} [finite G] [decidable_eq G] :
theorem zsmul_eq_zero_iff_modeq {G : Type u_1} [add_group G] {x : G} {n : } :
theorem zpow_eq_one_iff_modeq {G : Type u_1} [group G] {x : G} {n : } :
x ^ n = 1 n 0 [ZMOD (order_of x)]
theorem zpow_eq_zpow_iff_modeq {G : Type u_1} [group G] {x : G} {m n : } :
x ^ m = x ^ n m n [ZMOD (order_of x)]
theorem zsmul_eq_zsmul_iff_modeq {G : Type u_1} [add_group G] {x : G} {m n : } :
@[simp]
theorem injective_zsmul_iff_not_is_of_fin_order {G : Type u_1} [add_group G] {x : G} :
function.injective (λ (n : ), n x)
@[simp]
theorem injective_zpow_iff_not_is_of_fin_order {G : Type u_1} [group G] {x : G} :
function.injective (λ (n : ), x ^ n)
@[protected, instance]
noncomputable def decidable_zmultiples {G : Type u_1} [add_group G] {x : G} :
Equations
@[protected, instance]
noncomputable def decidable_zpowers {G : Type u_1} [group G] {x : G} :
decidable_pred (λ (_x : G), _x subgroup.zpowers x)
Equations
noncomputable def fin_equiv_zpowers {G : Type u_1} [group G] [finite G] (x : G) :

The equivalence between `fin (order_of x)` and `subgroup.zpowers x`, sending `i` to `x ^ i`.

Equations
noncomputable def fin_equiv_zmultiples {G : Type u_1} [add_group G] [finite G] (x : G) :

The equivalence between `fin (add_order_of a)` and `subgroup.zmultiples a`, sending `i` to `i • a`.

Equations
@[simp]
theorem fin_equiv_zpowers_apply {G : Type u_1} [group G] {x : G} [finite G] {n : fin (order_of x)} :
n = x ^ n, _⟩
@[simp]
theorem fin_equiv_zmultiples_apply {G : Type u_1} [add_group G] {x : G} [finite G] {n : fin (add_order_of x)} :
= n x, _⟩
@[simp]
theorem fin_equiv_zmultiples_symm_apply {G : Type u_1} [add_group G] [finite G] (x : G) (n : ) {hn : (m : ), m x = n x} :
.symm) n x, hn⟩ = , _⟩
@[simp]
theorem fin_equiv_zpowers_symm_apply {G : Type u_1} [group G] [finite G] (x : G) (n : ) {hn : (m : ), x ^ m = x ^ n} :
.symm) x ^ n, hn⟩ = n % , _⟩
noncomputable def zmultiples_equiv_zmultiples {G : Type u_1} [add_group G] {x y : G} [finite G] (h : = ) :

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

Equations
noncomputable def zpowers_equiv_zpowers {G : Type u_1} [group G] {x y : G} [finite G] (h : = ) :

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

Equations
@[simp]
theorem zmultiples_equiv_zmultiples_apply {G : Type u_1} [add_group G] {x y : G} [finite G] (h : = ) (n : ) :
n x, _⟩ = n y, _⟩
@[simp]
theorem zpowers_equiv_zpowers_apply {G : Type u_1} [group G] {x y : G} [finite G] (h : = ) (n : ) :
x ^ n, _⟩ = y ^ n, _⟩
theorem add_order_eq_card_zmultiples {G : Type u_1} [add_group G] {x : G} [fintype G] :

See also `nat.card_zmultiples`.

theorem order_eq_card_zpowers {G : Type u_1} [group G] {x : G} [fintype G] :

See also `nat.card_zpowers'`.

theorem order_of_dvd_card_univ {G : Type u_1} [group G] {x : G} [fintype G] :
theorem add_order_of_dvd_card_univ {G : Type u_1} [add_group G] {x : G} [fintype G] :
theorem add_order_of_dvd_nat_card {G : Type u_1} [add_group G] {x : G} :
theorem order_of_dvd_nat_card {G : Type u_1} [group G] {x : G} :
@[simp]
theorem pow_card_eq_one' {G : Type u_1} [group G] {x : G} :
x ^ = 1
@[simp]
theorem card_nsmul_eq_zero' {G : Type u_1} [add_group G] {x : G} :
x = 0
@[simp]
theorem pow_card_eq_one {G : Type u_1} [group G] {x : G} [fintype G] :
= 1
@[simp]
theorem card_nsmul_eq_zero {G : Type u_1} [add_group G] {x : G} [fintype G] :
= 0
theorem subgroup.pow_index_mem {G : Type u_1} [group G] (H : subgroup G) [H.normal] (g : G) :
g ^ H.index H
theorem add_subgroup.nsmul_index_mem {G : Type u_1} [add_group G] (H : add_subgroup G) [H.normal] (g : G) :
H.index g H
theorem nsmul_eq_mod_card {G : Type u_1} [add_group G] {x : G} [fintype G] (n : ) :
n x = (n % x
theorem pow_eq_mod_card {G : Type u_1} [group G] {x : G} [fintype G] (n : ) :
x ^ n = x ^ (n %
theorem zpow_eq_mod_card {G : Type u_1} [group G] {x : G} [fintype G] (n : ) :
x ^ n = x ^ (n % (fintype.card G))
theorem zsmul_eq_mod_card {G : Type u_1} [add_group G] {x : G} [fintype G] (n : ) :
n x = (n % (fintype.card G)) x
@[simp]
theorem pow_coprime_symm_apply {n : } {G : Type u_1} [group G] (h : (nat.card G).coprime n) (g : G) :
noncomputable def pow_coprime {n : } {G : Type u_1} [group G] (h : (nat.card G).coprime n) :
G G

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

Equations
@[simp]
theorem pow_coprime_apply {n : } {G : Type u_1} [group G] (h : (nat.card G).coprime n) (g : G) :
(pow_coprime h) g = g ^ n
@[simp]
theorem nsmul_coprime_symm_apply {n : } {G : Type u_1} [add_group G] (h : (nat.card G).coprime n) (g : G) :
@[simp]
theorem nsmul_coprime_apply {n : } {G : Type u_1} [add_group G] (h : (nat.card G).coprime n) (g : G) :
g = n g
noncomputable def nsmul_coprime {n : } {G : Type u_1} [add_group G] (h : (nat.card G).coprime n) :
G G

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

Equations
@[simp]
theorem pow_coprime_one {n : } {G : Type u_1} [group G] (h : (nat.card G).coprime n) :
@[simp]
theorem nsmul_coprime_zero {n : } {G : Type u_1} [add_group G] (h : (nat.card G).coprime n) :
0 = 0
@[simp]
theorem pow_coprime_inv {n : } {G : Type u_1} [group G] (h : (nat.card G).coprime n) {g : G} :
@[simp]
theorem nsmul_coprime_neg {n : } {G : Type u_1} [add_group G] (h : (nat.card G).coprime n) {g : G} :
(-g) = - g
theorem inf_eq_bot_of_coprime {G : Type u_1} [group G] {H K : subgroup G} [fintype H] [fintype K] (h : .coprime ) :
H K =
theorem add_inf_eq_bot_of_coprime {G : Type u_1} [add_group G] {H K : add_subgroup G} [fintype H] [fintype K] (h : .coprime ) :
H K =
theorem image_range_add_order_of {G : Type u_1} [add_group G] {x : G} [fintype G] [decidable_eq G] :
@[nolint]
theorem image_range_order_of {G : Type u_1} [group G] {x : G} [fintype G] [decidable_eq G] :
finset.image (λ (i : ), x ^ i) (finset.range (order_of x)) =

TODO: Generalise to `submonoid.powers`.

theorem pow_gcd_card_eq_one_iff {G : Type u_1} [group G] {x : G} {n : } [fintype G] :
x ^ n = 1 x ^ n.gcd (fintype.card G) = 1

TODO: Generalise to `finite` + `cancel_monoid`.

theorem gcd_nsmul_card_eq_zero_iff {G : Type u_1} [add_group G] {x : G} {n : } [fintype G] :
n x = 0 n.gcd (fintype.card G) x = 0

TODO: Generalise to `finite` + `cancel_add_monoid`

def add_submonoid_of_idempotent {M : Type u_1} [fintype 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
def submonoid_of_idempotent {M : Type u_1} [fintype M] (S : set M) (hS1 : S.nonempty) (hS2 : S * S = S) :

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

Equations
def add_subgroup_of_idempotent {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS1 : S.nonempty) (hS2 : S + S = S) :

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

Equations
def subgroup_of_idempotent {G : Type u_1} [group G] [fintype G] (S : set G) (hS1 : S.nonempty) (hS2 : S * S = S) :

A nonempty idempotent subset of a finite group is a subgroup

Equations
@[simp]
theorem smul_card_add_subgroup_coe {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS : S.nonempty) :
hS) =
def smul_card_add_subgroup {G : Type u_1} [add_group 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
• = have one_mem : 0 , from _,
@[simp]
theorem pow_card_subgroup_coe {G : Type u_1} [group G] [fintype G] (S : set G) (hS : S.nonempty) :
hS) =
def pow_card_subgroup {G : Type u_1} [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
• = have one_mem : 1 , from _,
theorem order_of_abs_ne_one {G : Type u_1} {x : G} (h : |x| 1) :
= 0
theorem linear_ordered_ring.order_of_le_two {G : Type u_1} {x : G} :
2
@[protected]
theorem prod.order_of {α : Type u_4} {β : Type u_5} [monoid α] [monoid β] (x : α × β) :
@[protected]
theorem prod.add_order_of {α : Type u_4} {β : Type u_5} [add_monoid α] [add_monoid β] (x : α × β) :
theorem order_of_fst_dvd_order_of {α : Type u_4} {β : Type u_5} [monoid α] [monoid β] {x : α × β} :
theorem add_order_of_fst_dvd_add_order_of {α : Type u_4} {β : Type u_5} [add_monoid α] [add_monoid β] {x : α × β} :
theorem order_of_snd_dvd_order_of {α : Type u_4} {β : Type u_5} [monoid α] [monoid β] {x : α × β} :
theorem add_order_of_snd_dvd_add_order_of {α : Type u_4} {β : Type u_5} [add_monoid α] [add_monoid β] {x : α × β} :
theorem is_of_fin_order.fst {α : Type u_4} {β : Type u_5} [monoid α] [monoid β] {x : α × β} (hx : is_of_fin_order x) :
theorem is_of_fin_add_order.fst {α : Type u_4} {β : Type u_5} [add_monoid α] [add_monoid β] {x : α × β} (hx : is_of_fin_add_order x) :
theorem is_of_fin_add_order.snd {α : Type u_4} {β : Type u_5} [add_monoid α] [add_monoid β] {x : α × β} (hx : is_of_fin_add_order x) :
theorem is_of_fin_order.snd {α : Type u_4} {β : Type u_5} [monoid α] [monoid β] {x : α × β} (hx : is_of_fin_order x) :
theorem is_of_fin_order.prod_mk {α : Type u_4} {β : Type u_5} [monoid α] [monoid β] {a : α} {b : β} :
theorem is_of_fin_add_order.prod_mk {α : Type u_4} {β : Type u_5} [add_monoid α] [add_monoid β] {a : α} {b : β} :