group_theory.order_of_element

source

theorem is_periodic_pt_add_iff_nsmul_eq_zero {G : Type u} {n : ℕ} [add_monoid G] (x : G) :

function.is_periodic_pt (has_add.add x) n 0 ↔ n • x = 0

source

theorem is_periodic_pt_mul_iff_pow_eq_one {G : Type u} {n : ℕ} [monoid G] (x : G) :

function.is_periodic_pt (has_mul.mul x) n 1 ↔ x ^ n = 1

source

def is_of_fin_add_order {A : Type v} [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

is_of_fin_add_order a = (0 ∈ function.periodic_pts (has_add.add a))

source

def is_of_fin_order {G : Type u} [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

is_of_fin_order x = (1 ∈ function.periodic_pts (has_mul.mul x))

source

theorem is_of_fin_add_order_of_mul_iff {G : Type u} {x : G} [monoid G] :

is_of_fin_add_order (⇑additive.of_mul x) ↔ is_of_fin_order x

source

theorem is_of_fin_order_of_add_iff {A : Type v} {a : A} [add_monoid A] :

is_of_fin_order (⇑multiplicative.of_add a) ↔ is_of_fin_add_order a

source

theorem is_of_fin_order_iff_pow_eq_one {G : Type u} [monoid G] (x : G) :

is_of_fin_order x ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

source

theorem is_of_fin_add_order_iff_nsmul_eq_zero {G : Type u} [add_monoid G] (x : G) :

is_of_fin_add_order x ↔ ∃ (n : ℕ), 0 < n ∧ n • x = 0

source

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

is_of_fin_add_order x ↔ is_of_fin_add_order ↑x

source

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

is_of_fin_order x ↔ is_of_fin_order ↑x

Elements of finite order are of finite order in submonoids.

source

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

is_of_fin_add_order (⇑f x)

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

source

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

is_of_fin_order (⇑f x)

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

source

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

is_of_fin_order (x i)

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

source

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

is_of_fin_add_order (x i)

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

source

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

is_of_fin_add_order 0

0 is of finite order in any additive monoid.

source

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

is_of_fin_order 1

1 is of finite order in any monoid.

source

noncomputable def order_of {G : Type u} [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

order_of x = function.minimal_period (has_mul.mul x) 1

source

noncomputable def add_order_of {G : Type u} [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

add_order_of x = function.minimal_period (has_add.add x) 0

source

@[simp]

theorem add_order_of_of_mul_eq_order_of {G : Type u} [monoid G] (x : G) :

add_order_of (⇑additive.of_mul x) = order_of x

source

@[simp]

theorem order_of_of_add_eq_add_order_of {A : Type v} [add_monoid A] (a : A) :

order_of (⇑multiplicative.of_add a) = add_order_of a

source

theorem add_order_of_pos' {G : Type u} {x : G} [add_monoid G] (h : is_of_fin_add_order x) :

0 < add_order_of x

source

theorem order_of_pos' {G : Type u} {x : G} [monoid G] (h : is_of_fin_order x) :

0 < order_of x

source

theorem pow_order_of_eq_one {G : Type u} [monoid G] (x : G) :

x ^ order_of x = 1

source

theorem add_order_of_nsmul_eq_zero {G : Type u} [add_monoid G] (x : G) :

add_order_of x • x = 0

source

theorem order_of_eq_zero {G : Type u} {x : G} [monoid G] (h : ¬is_of_fin_order x) :

order_of x = 0

source

theorem add_order_of_eq_zero {G : Type u} {x : G} [add_monoid G] (h : ¬is_of_fin_add_order x) :

add_order_of x = 0

source

theorem add_order_of_eq_zero_iff {G : Type u} {x : G} [add_monoid G] :

add_order_of x = 0 ↔ ¬is_of_fin_add_order x

source

theorem order_of_eq_zero_iff {G : Type u} {x : G} [monoid G] :

order_of x = 0 ↔ ¬is_of_fin_order x

source

theorem order_of_eq_zero_iff' {G : Type u} {x : G} [monoid G] :

order_of x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

source

theorem add_order_of_eq_zero_iff' {G : Type u} {x : G} [add_monoid G] :

add_order_of x = 0 ↔ ∀ (n : ℕ), 0 < n → n • x ≠ 0

source

theorem add_order_of_pos_iff {G : Type u} {x : G} [add_monoid G] :

0 < add_order_of x ↔ is_of_fin_add_order x

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

source

theorem order_of_pos_iff {G : Type u} {x : G} [monoid G] :

0 < order_of x ↔ is_of_fin_order x

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

source

theorem pow_ne_one_of_lt_order_of' {G : Type u} {x : G} {n : ℕ} [monoid G] (n0 : n ≠ 0) (h : n < order_of x) :

x ^ n ≠ 1

source

theorem nsmul_ne_zero_of_lt_add_order_of' {G : Type u} {x : G} {n : ℕ} [add_monoid G] (n0 : n ≠ 0) (h : n < add_order_of x) :

n • x ≠ 0

source

theorem add_order_of_le_of_nsmul_eq_zero {G : Type u} {x : G} {n : ℕ} [add_monoid G] (hn : 0 < n) (h : n • x = 0) :

add_order_of x ≤ n

source

theorem order_of_le_of_pow_eq_one {G : Type u} {x : G} {n : ℕ} [monoid G] (hn : 0 < n) (h : x ^ n = 1) :

order_of x ≤ n

source

@[simp]

theorem order_of_one {G : Type u} [monoid G] :

order_of 1 = 1

source

@[simp]

theorem order_of_zero {G : Type u} [add_monoid G] :

add_order_of 0 = 1

source

@[simp]

theorem order_of_eq_one_iff {G : Type u} {x : G} [monoid G] :

order_of x = 1 ↔ x = 1

source

@[simp]

theorem add_monoid.order_of_eq_one_iff {G : Type u} {x : G} [add_monoid G] :

add_order_of x = 1 ↔ x = 0

source

theorem pow_eq_mod_order_of {G : Type u} {x : G} [monoid G] {n : ℕ} :

x ^ n = x ^ (n % order_of x)

source

theorem nsmul_eq_mod_add_order_of {G : Type u} {x : G} [add_monoid G] {n : ℕ} :

n • x = (n % add_order_of x) • x

source

theorem order_of_dvd_of_pow_eq_one {G : Type u} {x : G} {n : ℕ} [monoid G] (h : x ^ n = 1) :

order_of x ∣ n

source

theorem add_order_of_dvd_of_nsmul_eq_zero {G : Type u} {x : G} {n : ℕ} [add_monoid G] (h : n • x = 0) :

add_order_of x ∣ n

source

theorem add_order_of_dvd_iff_nsmul_eq_zero {G : Type u} {x : G} [add_monoid G] {n : ℕ} :

add_order_of x ∣ n ↔ n • x = 0

source

theorem order_of_dvd_iff_pow_eq_one {G : Type u} {x : G} [monoid G] {n : ℕ} :

order_of x ∣ n ↔ x ^ n = 1

source

theorem add_order_of_map_dvd {G : Type u} [add_monoid G] {H : Type u_1} [add_monoid H] (ψ : G →+ H) (x : G) :

add_order_of (⇑ψ x) ∣ add_order_of x

source

theorem order_of_map_dvd {G : Type u} [monoid G] {H : Type u_1} [monoid H] (ψ : G →* H) (x : G) :

order_of (⇑ψ x) ∣ order_of x

source

theorem exists_pow_eq_self_of_coprime {G : Type u} {x : G} {n : ℕ} [monoid G] (h : n.coprime (order_of x)) :

∃ (m : ℕ), (x ^ n) ^ m = x

source

theorem exists_nsmul_eq_self_of_coprime {G : Type u} {x : G} {n : ℕ} [add_monoid G] (h : n.coprime (add_order_of x)) :

∃ (m : ℕ), m • n • x = x

source

theorem add_order_of_eq_of_nsmul_and_div_prime_nsmul {G : Type u} {x : G} {n : ℕ} [add_monoid G] (hn : 0 < n) (hx : n • x = 0) (hd : ∀ (p : ℕ), nat.prime p → p ∣ n → (n / p) • x ≠ 0) :

add_order_of x = n

source

theorem order_of_eq_of_pow_and_pow_div_prime {G : Type u} {x : G} {n : ℕ} [monoid G] (hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ (p : ℕ), nat.prime p → p ∣ n → x ^ (n / p) ≠ 1) :

order_of x = n

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

source

theorem order_of_eq_order_of_iff {G : Type u} {x : G} [monoid G] {H : Type u_1} [monoid H] {y : H} :

order_of x = order_of y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

source

theorem add_order_of_eq_add_order_of_iff {G : Type u} {x : G} [add_monoid G] {H : Type u_1} [add_monoid H] {y : H} :

add_order_of x = add_order_of y ↔ ∀ (n : ℕ), n • x = 0 ↔ n • y = 0

source

theorem order_of_injective {G : Type u} [monoid G] {H : Type u_1} [monoid H] (f : G →* H) (hf : function.injective ⇑f) (x : G) :

order_of (⇑f x) = order_of x

source

theorem add_order_of_injective {G : Type u} [add_monoid G] {H : Type u_1} [add_monoid H] (f : G →+ H) (hf : function.injective ⇑f) (x : G) :

add_order_of (⇑f x) = add_order_of x

source

@[simp, norm_cast]

theorem order_of_submonoid {G : Type u} [monoid G] {H : submonoid G} (y : ↥H) :

order_of ↑y = order_of y

source

@[simp, norm_cast]

theorem order_of_add_submonoid {G : Type u} [add_monoid G] {H : add_submonoid G} (y : ↥H) :

add_order_of ↑y = add_order_of y

source

theorem order_of_units {G : Type u} [monoid G] {y : Gˣ} :

order_of ↑y = order_of y

source

theorem order_of_add_units {G : Type u} [add_monoid G] {y : add_units G} :

add_order_of ↑y = add_order_of y

source

theorem add_order_of_nsmul' {G : Type u} (x : G) {n : ℕ} [add_monoid G] (h : n ≠ 0) :

add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n

source

theorem order_of_pow' {G : Type u} (x : G) {n : ℕ} [monoid G] (h : n ≠ 0) :

order_of (x ^ n) = order_of x / (order_of x).gcd n

source

theorem add_order_of_nsmul'' {G : Type u} (x : G) (n : ℕ) [add_monoid G] (h : is_of_fin_add_order x) :

add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n

source

theorem order_of_pow'' {G : Type u} (x : G) (n : ℕ) [monoid G] (h : is_of_fin_order x) :

order_of (x ^ n) = order_of x / (order_of x).gcd n

source

theorem commute.order_of_mul_dvd_lcm {G : Type u} [monoid G] {x y : G} (h : commute x y) :

order_of (x * y) ∣ (order_of x).lcm (order_of y)

source

theorem add_commute.order_of_add_dvd_lcm {G : Type u} [add_monoid G] {x y : G} (h : add_commute x y) :

add_order_of (x + y) ∣ (add_order_of x).lcm (add_order_of y)

source

theorem commute.order_of_mul_dvd_mul_order_of {G : Type u} [monoid G] {x y : G} (h : commute x y) :

order_of (x * y) ∣ order_of x * order_of y

source

theorem add_commute.add_order_of_add_dvd_mul_add_order_of {G : Type u} [add_monoid G] {x y : G} (h : add_commute x y) :

add_order_of (x + y) ∣ add_order_of x * add_order_of y

source

theorem add_commute.add_order_of_add_eq_mul_add_order_of_of_coprime {G : Type u} [add_monoid G] {x y : G} (h : add_commute x y) (hco : (add_order_of x).coprime (add_order_of y)) :

add_order_of (x + y) = add_order_of x * add_order_of y

source

theorem commute.order_of_mul_eq_mul_order_of_of_coprime {G : Type u} [monoid G] {x y : G} (h : commute x y) (hco : (order_of x).coprime (order_of y)) :

order_of (x * y) = order_of x * order_of y

source

theorem add_commute.is_of_fin_order_add {G : Type u} {y : G} [add_monoid G] {x : G} (h : add_commute x y) (hx : is_of_fin_add_order x) (hy : is_of_fin_add_order y) :

is_of_fin_add_order (x + y)

Commuting elements of finite additive order are closed under addition.

source

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

is_of_fin_order (x * y)

Commuting elements of finite order are closed under multiplication.

source

theorem add_order_of_eq_prime {G : Type u} {x : G} [add_monoid G] {p : ℕ} [hp : fact (nat.prime p)] (hg : p • x = 0) (hg1 : x ≠ 0) :

add_order_of x = p

source

theorem order_of_eq_prime {G : Type u} {x : G} [monoid G] {p : ℕ} [hp : fact (nat.prime p)] (hg : x ^ p = 1) (hg1 : x ≠ 1) :

order_of x = p

source

theorem add_order_of_eq_prime_pow {G : Type u} {x : G} {n : ℕ} [add_monoid G] {p : ℕ} [hp : fact (nat.prime p)] (hnot : ¬p ^ n • x = 0) (hfin : p ^ (n + 1) • x = 0) :

add_order_of x = p ^ (n + 1)

source

theorem order_of_eq_prime_pow {G : Type u} {x : G} {n : ℕ} [monoid G] {p : ℕ} [hp : fact (nat.prime p)] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :

order_of x = p ^ (n + 1)

source

theorem exists_add_order_of_eq_prime_pow_iff {G : Type u} {x : G} [add_monoid G] {p : ℕ} [hp : fact (nat.prime p)] :

(∃ (k : ℕ), add_order_of x = p ^ k) ↔ ∃ (m : ℕ), p ^ m • x = 0

source

theorem exists_order_of_eq_prime_pow_iff {G : Type u} {x : G} [monoid G] {p : ℕ} [hp : fact (nat.prime p)] :

(∃ (k : ℕ), order_of x = p ^ k) ↔ ∃ (m : ℕ), x ^ p ^ m = 1

source

theorem nsmul_injective_of_lt_add_order_of {G : Type u} (x : G) {n m : ℕ} [add_left_cancel_monoid G] (hn : n < add_order_of x) (hm : m < add_order_of x) (eq : n • x = m • x) :

n = m

source

theorem pow_injective_of_lt_order_of {G : Type u} (x : G) {n m : ℕ} [left_cancel_monoid G] (hn : n < order_of x) (hm : m < order_of x) (eq : x ^ n = x ^ m) :

n = m

source

theorem mem_powers_iff_mem_range_order_of' {G : Type u} (x y : G) [left_cancel_monoid G] [decidable_eq G] (hx : 0 < order_of x) :

y ∈ submonoid.powers x ↔ y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))

source

theorem mem_multiples_iff_mem_range_add_order_of' {G : Type u} (x y : G) [add_left_cancel_monoid G] [decidable_eq G] (hx : 0 < add_order_of x) :

y ∈ add_submonoid.multiples x ↔ y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))

source

theorem pow_eq_one_iff_modeq {G : Type u} (x : G) {n : ℕ} [left_cancel_monoid G] :

x ^ n = 1 ↔ n ≡ 0 [MOD order_of x]

source

theorem pow_eq_pow_iff_modeq {G : Type u} (x : G) {n m : ℕ} [left_cancel_monoid G] :

x ^ n = x ^ m ↔ n ≡ m [MOD order_of x]

source

theorem is_of_fin_order.inv {G : Type u} [group G] {x : G} (hx : is_of_fin_order x) :

is_of_fin_order x⁻¹

Inverses of elements of finite order have finite order.

source

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

is_of_fin_add_order (-x)

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

source

@[simp]

theorem is_of_fin_order_inv_iff {G : Type u} [group G] {x : G} :

is_of_fin_order x⁻¹ ↔ is_of_fin_order x

Inverses of elements of finite order have finite order.

source

@[simp]

theorem is_of_fin_order_neg_iff {G : Type u} [add_group G] {x : G} :

is_of_fin_add_order (-x) ↔ is_of_fin_add_order x

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

source

theorem order_of_dvd_iff_zpow_eq_one {G : Type u} {x : G} [group G] {i : ℤ} :

↑(order_of x) ∣ i ↔ x ^ i = 1

source

theorem add_order_of_dvd_iff_zsmul_eq_zero {G : Type u} {x : G} [add_group G] {i : ℤ} :

↑(add_order_of x) ∣ i ↔ i • x = 0

source

@[simp]

theorem order_of_neg {G : Type u} [add_group G] (x : G) :

add_order_of (-x) = add_order_of x

source

@[simp]

theorem order_of_inv {G : Type u} [group G] (x : G) :

order_of x⁻¹ = order_of x

source

@[simp, norm_cast]

theorem order_of_add_subgroup {G : Type u} [add_group G] {H : add_subgroup G} (y : ↥H) :

add_order_of ↑y = add_order_of y

source

@[simp, norm_cast]

theorem order_of_subgroup {G : Type u} [group G] {H : subgroup G} (y : ↥H) :

order_of ↑y = order_of y

source

theorem zsmul_eq_mod_add_order_of {G : Type u} {x : G} [add_group G] {i : ℤ} :

i • x = (i % ↑(add_order_of x)) • x

source

theorem zpow_eq_mod_order_of {G : Type u} {x : G} [group G] {i : ℤ} :

x ^ i = x ^ (i % ↑(order_of x))

source

theorem pow_inj_iff_of_order_of_eq_zero {G : Type u} {x : G} [group G] (h : order_of x = 0) {n m : ℕ} :

x ^ n = x ^ m ↔ n = m

source

theorem nsmul_inj_iff_of_add_order_of_eq_zero {G : Type u} {x : G} [add_group G] (h : add_order_of x = 0) {n m : ℕ} :

n • x = m • x ↔ n = m

source

theorem nsmul_inj_mod {G : Type u} {x : G} [add_group G] {n m : ℕ} :

n • x = m • x ↔ n % add_order_of x = m % add_order_of x

source

theorem pow_inj_mod {G : Type u} {x : G} [group G] {n m : ℕ} :

x ^ n = x ^ m ↔ n % order_of x = m % order_of x

source

theorem is_of_fin_order.mul {G : Type u} {x y : G} [comm_monoid G] (hx : is_of_fin_order x) (hy : is_of_fin_order y) :

is_of_fin_order (x * y)

Elements of finite order are closed under multiplication.

source

theorem is_of_fin_add_order.add {G : Type u} {x y : G} [add_comm_monoid G] (hx : is_of_fin_add_order x) (hy : is_of_fin_add_order y) :

is_of_fin_add_order (x + y)

Elements of finite additive order are closed under addition.

source

theorem sum_card_order_of_eq_card_pow_eq_one {G : Type u} {n : ℕ} [fintype G] [monoid G] [decidable_eq G] (hn : 0 < n) :

(finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ)).sum (λ (m : ℕ), (finset.filter (λ (x : G), order_of x = m) finset.univ).card) = (finset.filter (λ (x : G), x ^ n = 1) finset.univ).card

source

theorem sum_card_add_order_of_eq_card_nsmul_eq_zero {G : Type u} {n : ℕ} [fintype G] [add_monoid G] [decidable_eq G] (hn : 0 < n) :

(finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ)).sum (λ (m : ℕ), (finset.filter (λ (x : G), add_order_of x = m) finset.univ).card) = (finset.filter (λ (x : G), n • x = 0) finset.univ).card

source

theorem exists_pow_eq_one {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :

is_of_fin_order x

source

theorem exists_nsmul_eq_zero {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) :

is_of_fin_add_order x

source

theorem order_of_le_card_univ {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] :

order_of x ≤ fintype.card G

source

theorem add_order_of_le_card_univ {G : Type u} {x : G} [fintype G] [add_left_cancel_monoid G] :

add_order_of x ≤ fintype.card G

source

theorem order_of_pos {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :

0 < order_of x

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.

source

theorem add_order_of_pos {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) :

0 < add_order_of x

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.

source

theorem add_order_of_nsmul {G : Type u} {n : ℕ} [fintype G] [add_left_cancel_monoid G] (x : G) :

add_order_of (n • x) = add_order_of x / (add_order_of x).gcd n

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.

source

theorem order_of_pow {G : Type u} {n : ℕ} [fintype G] [left_cancel_monoid G] (x : G) :

order_of (x ^ n) = order_of x / (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.

source

theorem mem_multiples_iff_mem_range_add_order_of {G : Type u} {x y : G} [fintype G] [add_left_cancel_monoid G] [decidable_eq G] :

y ∈ add_submonoid.multiples x ↔ y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))

source

theorem mem_powers_iff_mem_range_order_of {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :

y ∈ submonoid.powers x ↔ y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))

source

@[protected, instance]

noncomputable def decidable_multiples {G : Type u} {x : G} [fintype G] [add_left_cancel_monoid G] [decidable_eq G] :

decidable_pred (λ (_x : G), _x ∈ add_submonoid.multiples x)

Equations

decidable_multiples = id (λ (y : G), decidable_of_iff' (y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))) _)

source

@[protected, instance]

noncomputable def decidable_powers {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :

decidable_pred (λ (_x : G), _x ∈ submonoid.powers x)

Equations

decidable_powers = id (λ (y : G), decidable_of_iff' (y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))) _)

source

noncomputable def fin_equiv_multiples {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) :

fin (add_order_of x) ≃ ↥↑(add_submonoid.multiples x)

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

Equations

fin_equiv_multiples x = equiv.of_bijective (λ (n : fin (add_order_of x)), ⟨↑n • x, _⟩) _

source

noncomputable def fin_equiv_powers {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :

fin (order_of x) ≃ ↥↑(submonoid.powers x)

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

Equations

fin_equiv_powers x = equiv.of_bijective (λ (n : fin (order_of x)), ⟨x ^ ↑n, _⟩) _

source

@[simp]

theorem fin_equiv_multiples_apply {G : Type u} [fintype G] [add_left_cancel_monoid G] {x : G} {n : fin (add_order_of x)} :

⇑(fin_equiv_multiples x) n = ⟨↑n • x, _⟩

source

@[simp]

theorem fin_equiv_powers_apply {G : Type u} [fintype G] [left_cancel_monoid G] {x : G} {n : fin (order_of x)} :

⇑(fin_equiv_powers x) n = ⟨x ^ ↑n, _⟩

source

@[simp]

theorem fin_equiv_multiples_symm_apply {G : Type u} [fintype G] [add_left_cancel_monoid G] (x : G) (n : ℕ) {hn : ∃ (m : ℕ), m • x = n • x} :

⇑((fin_equiv_multiples x).symm) ⟨n • x, hn⟩ = ⟨n % add_order_of x, _⟩

source

@[simp]

theorem fin_equiv_powers_symm_apply {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) (n : ℕ) {hn : ∃ (m : ℕ), x ^ m = x ^ n} :

⇑((fin_equiv_powers x).symm) ⟨x ^ n, hn⟩ = ⟨n % order_of x, _⟩

source

noncomputable def powers_equiv_powers {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] (h : order_of x = order_of y) :

↥↑(submonoid.powers x) ≃ ↥↑(submonoid.powers y)

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

Equations

powers_equiv_powers h = (fin_equiv_powers x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_powers y))

source

noncomputable def multiples_equiv_multiples {G : Type u} {x y : G} [fintype G] [add_left_cancel_monoid G] (h : add_order_of x = add_order_of y) :

↥↑(add_submonoid.multiples x) ≃ ↥↑(add_submonoid.multiples y)

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

Equations

multiples_equiv_multiples h = (fin_equiv_multiples x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_multiples y))

source

@[simp]

theorem powers_equiv_powers_apply {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] (h : order_of x = order_of y) (n : ℕ) :

⇑(powers_equiv_powers h) ⟨x ^ n, _⟩ = ⟨y ^ n, _⟩

source

@[simp]

theorem multiples_equiv_multiples_apply {G : Type u} {x y : G} [fintype G] [add_left_cancel_monoid G] (h : add_order_of x = add_order_of y) (n : ℕ) :

⇑(multiples_equiv_multiples h) ⟨n • x, _⟩ = ⟨n • y, _⟩

source

theorem add_order_of_eq_card_multiples {G : Type u} {x : G} [fintype G] [add_left_cancel_monoid G] [decidable_eq G] :

add_order_of x = fintype.card ↥↑(add_submonoid.multiples x)

source

theorem order_eq_card_powers {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :

order_of x = fintype.card ↥↑(submonoid.powers x)

source

theorem exists_zpow_eq_one {G : Type u} [fintype G] [group G] (x : G) :

∃ (i : ℤ) (H : i ≠ 0), x ^ i = 1

source

theorem exists_zsmul_eq_zero {G : Type u} [fintype G] [add_group G] (x : G) :

∃ (i : ℤ) (H : i ≠ 0), i • x = 0

source

theorem mem_multiples_iff_mem_zmultiples {G : Type u} {x y : G} [fintype G] [add_group G] :

y ∈ add_submonoid.multiples x ↔ y ∈ add_subgroup.zmultiples x

source

theorem mem_powers_iff_mem_zpowers {G : Type u} {x y : G} [fintype G] [group G] :

y ∈ submonoid.powers x ↔ y ∈ subgroup.zpowers x

source

theorem multiples_eq_zmultiples {G : Type u} [fintype G] [add_group G] (x : G) :

↑(add_submonoid.multiples x) = ↑(add_subgroup.zmultiples x)

source

theorem powers_eq_zpowers {G : Type u} [fintype G] [group G] (x : G) :

↑(submonoid.powers x) = ↑(subgroup.zpowers x)

source

theorem mem_zmultiples_iff_mem_range_add_order_of {G : Type u} {x y : G} [fintype G] [add_group G] [decidable_eq G] :

y ∈ add_subgroup.zmultiples x ↔ y ∈ finset.image (λ (ᾰ : ℕ), ᾰ • x) (finset.range (add_order_of x))

source

theorem mem_zpowers_iff_mem_range_order_of {G : Type u} {x y : G} [fintype G] [group G] [decidable_eq G] :

y ∈ subgroup.zpowers x ↔ y ∈ finset.image (has_pow.pow x) (finset.range (order_of x))

source

@[protected, instance]

noncomputable def decidable_zmultiples {G : Type u} {x : G} [fintype G] [add_group G] [decidable_eq G] :

decidable_pred (λ (_x : G), _x ∈ add_subgroup.zmultiples x)

Equations

decidable_zmultiples = decidable_zmultiples._proof_1.mpr (decidable_zmultiples._proof_2.mpr decidable_multiples)

source

@[protected, instance]

noncomputable def decidable_zpowers {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :

decidable_pred (λ (_x : G), _x ∈ subgroup.zpowers x)

Equations

decidable_zpowers = decidable_zpowers._proof_1.mpr (decidable_zpowers._proof_2.mpr decidable_powers)

source

noncomputable def fin_equiv_zpowers {G : Type u} [fintype G] [group G] (x : G) :

fin (order_of x) ≃ ↥↑(subgroup.zpowers x)

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

Equations

fin_equiv_zpowers x = (fin_equiv_powers x).trans (equiv.set.of_eq _)

source

noncomputable def fin_equiv_zmultiples {G : Type u} [fintype G] [add_group G] (x : G) :

fin (add_order_of x) ≃ ↥↑(add_subgroup.zmultiples x)

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

Equations

fin_equiv_zmultiples x = (fin_equiv_multiples x).trans (equiv.set.of_eq _)

source

@[simp]

theorem fin_equiv_zpowers_apply {G : Type u} {x : G} [fintype G] [group G] {n : fin (order_of x)} :

⇑(fin_equiv_zpowers x) n = ⟨x ^ ↑n, _⟩

source

@[simp]

theorem fin_equiv_zmultiples_apply {G : Type u} {x : G} [fintype G] [add_group G] {n : fin (add_order_of x)} :

⇑(fin_equiv_zmultiples x) n = ⟨↑n • x, _⟩

source

@[simp]

theorem fin_equiv_zmultiples_symm_apply {G : Type u} [fintype G] [add_group G] (x : G) (n : ℕ) {hn : ∃ (m : ℤ), m • x = n • x} :

⇑((fin_equiv_zmultiples x).symm) ⟨n • x, hn⟩ = ⟨n % add_order_of x, _⟩

source

@[simp]

theorem fin_equiv_zpowers_symm_apply {G : Type u} [fintype G] [group G] (x : G) (n : ℕ) {hn : ∃ (m : ℤ), x ^ m = x ^ n} :

⇑((fin_equiv_zpowers x).symm) ⟨x ^ n, hn⟩ = ⟨n % order_of x, _⟩

source

noncomputable def zmultiples_equiv_zmultiples {G : Type u} {x y : G} [fintype G] [add_group G] (h : add_order_of x = add_order_of y) :

↥↑(add_subgroup.zmultiples x) ≃ ↥↑(add_subgroup.zmultiples y)

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

Equations

zmultiples_equiv_zmultiples h = (fin_equiv_zmultiples x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_zmultiples y))

source

noncomputable def zpowers_equiv_zpowers {G : Type u} {x y : G} [fintype G] [group G] (h : order_of x = order_of y) :

↥↑(subgroup.zpowers x) ≃ ↥↑(subgroup.zpowers y)

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

Equations

zpowers_equiv_zpowers h = (fin_equiv_zpowers x).symm.trans ((fin.cast h).to_equiv.trans (fin_equiv_zpowers y))

source

@[simp]

theorem zmultiples_equiv_zmultiples_apply {G : Type u} {x y : G} [fintype G] [add_group G] (h : add_order_of x = add_order_of y) (n : ℕ) :

⇑(zmultiples_equiv_zmultiples h) ⟨n • x, _⟩ = ⟨n • y, _⟩

source

@[simp]

theorem zpowers_equiv_zpowers_apply {G : Type u} {x y : G} [fintype G] [group G] (h : order_of x = order_of y) (n : ℕ) :

⇑(zpowers_equiv_zpowers h) ⟨x ^ n, _⟩ = ⟨y ^ n, _⟩

source

theorem add_order_eq_card_zmultiples {G : Type u} {x : G} [fintype G] [add_group G] [decidable_eq G] :

add_order_of x = fintype.card ↥(add_subgroup.zmultiples x)

source

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

order_of x = fintype.card ↥(subgroup.zpowers x)

source

theorem order_of_dvd_card_univ {G : Type u} {x : G} [fintype G] [group G] :

order_of x ∣ fintype.card G

source

theorem add_order_of_dvd_card_univ {G : Type u} {x : G} [fintype G] [add_group G] :

add_order_of x ∣ fintype.card G

source

@[simp]

theorem pow_card_eq_one {G : Type u} {x : G} [fintype G] [group G] :

x ^ fintype.card G = 1

source

@[simp]

theorem card_nsmul_eq_zero {G : Type u} {x : G} [fintype G] [add_group G] :

fintype.card G • x = 0

source

theorem subgroup.pow_index_mem {G : Type u_1} [group G] (H : subgroup G) [fintype (G ⧸ H)] [H.normal] (g : G) :

g ^ H.index ∈ H

source

theorem add_subgroup.nsmul_index_mem {G : Type u_1} [add_group G] (H : add_subgroup G) [fintype (G ⧸ H)] [H.normal] (g : G) :

H.index • g ∈ H

source

theorem nsmul_eq_mod_card {G : Type u} {x : G} [fintype G] [add_group G] (n : ℕ) :

n • x = (n % fintype.card G) • x

source

theorem pow_eq_mod_card {G : Type u} {x : G} [fintype G] [group G] (n : ℕ) :

x ^ n = x ^ (n % fintype.card G)

source

theorem zpow_eq_mod_card {G : Type u} {x : G} [fintype G] [group G] (n : ℤ) :

x ^ n = x ^ (n % ↑(fintype.card G))

source

theorem zsmul_eq_mod_card {G : Type u} {x : G} [fintype G] [add_group G] (n : ℤ) :

n • x = (n % ↑(fintype.card G)) • x

source

@[simp]

theorem pow_coprime_symm_apply {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) (g : G) :

⇑((pow_coprime h).symm) g = g ^ (fintype.card G).gcd_b n

source

def pow_coprime {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) :

G ≃ G

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

Equations

pow_coprime h = {to_fun := λ (g : G), g ^ n, inv_fun := λ (g : G), g ^ (fintype.card G).gcd_b n, left_inv := _, right_inv := _}

source

@[simp]

theorem pow_coprime_apply {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) (g : G) :

⇑(pow_coprime h) g = g ^ n

source

@[simp]

theorem nsmul_coprime_symm_apply {G : Type u} {n : ℕ} [fintype G] [add_group G] (h : (fintype.card G).coprime n) (g : G) :

⇑((nsmul_coprime h).symm) g = (fintype.card G).gcd_b n • g

source

@[simp]

theorem nsmul_coprime_apply {G : Type u} {n : ℕ} [fintype G] [add_group G] (h : (fintype.card G).coprime n) (g : G) :

⇑(nsmul_coprime h) g = n • g

source

def nsmul_coprime {G : Type u} {n : ℕ} [fintype G] [add_group G] (h : (fintype.card G).coprime n) :

G ≃ G

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

Equations

nsmul_coprime h = {to_fun := λ (g : G), n • g, inv_fun := λ (g : G), (fintype.card G).gcd_b n • g, left_inv := _, right_inv := _}

source

@[simp]

theorem pow_coprime_one {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) :

⇑(pow_coprime h) 1 = 1

source

@[simp]

theorem nsmul_coprime_zero {G : Type u} {n : ℕ} [fintype G] [add_group G] (h : (fintype.card G).coprime n) :

⇑(nsmul_coprime h) 0 = 0

source

@[simp]

theorem pow_coprime_inv {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) {g : G} :

⇑(pow_coprime h) g⁻¹ = (⇑(pow_coprime h) g)⁻¹

source

@[simp]

theorem nsmul_coprime_neg {G : Type u} {n : ℕ} [fintype G] [add_group G] (h : (fintype.card G).coprime n) {g : G} :

⇑(nsmul_coprime h) (-g) = -⇑(nsmul_coprime h) g

source

theorem inf_eq_bot_of_coprime {G : Type u_1} [group G] {H K : subgroup G} [fintype ↥H] [fintype ↥K] (h : (fintype.card ↥H).coprime (fintype.card ↥K)) :

H ⊓ K = ⊥

source

theorem add_inf_eq_bot_of_coprime {G : Type u_1} [add_group G] {H K : add_subgroup G} [fintype ↥H] [fintype ↥K] (h : (fintype.card ↥H).coprime (fintype.card ↥K)) :

H ⊓ K = ⊥

source

theorem image_range_add_order_of {G : Type u} {x : G} [fintype G] [add_group G] [decidable_eq G] :

finset.image (λ (i : ℕ), i • x) (finset.range (add_order_of x)) = ↑(add_subgroup.zmultiples x).to_finset

source

theorem image_range_order_of {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :

finset.image (λ (i : ℕ), x ^ i) (finset.range (order_of x)) = ↑(subgroup.zpowers x).to_finset

TODO: Generalise to submonoid.powers.

source

theorem pow_gcd_card_eq_one_iff {G : Type u} {x : G} {n : ℕ} [fintype G] [group G] :

x ^ n = 1 ↔ x ^ n.gcd (fintype.card G) = 1

TODO: Generalise to finite_cancel_monoid.

source

theorem gcd_nsmul_card_eq_zero_iff {G : Type u} {x : G} {n : ℕ} [fintype G] [add_group G] :

n • x = 0 ↔ n.gcd (fintype.card G) • x = 0

source

def add_submonoid_of_idempotent {M : Type u_1} [add_left_cancel_monoid M] [fintype M] (S : set M) (hS1 : S.nonempty) (hS2 : S + S = S) :

add_submonoid M

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

Equations

add_submonoid_of_idempotent S hS1 hS2 = have pow_mem : ∀ (a : M), a ∈ S → ∀ (n : ℕ), (n + 1) • a ∈ S, from _, {carrier := S, add_mem' := _, zero_mem' := _}

source

def submonoid_of_idempotent {M : Type u_1} [left_cancel_monoid M] [fintype M] (S : set M) (hS1 : S.nonempty) (hS2 : S * S = S) :

submonoid M

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

Equations

submonoid_of_idempotent S hS1 hS2 = have pow_mem : ∀ (a : M), a ∈ S → ∀ (n : ℕ), a ^ (n + 1) ∈ S, from _, {carrier := S, mul_mem' := _, one_mem' := _}

source

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

add_subgroup G

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

Equations

add_subgroup_of_idempotent S hS1 hS2 = {carrier := S, add_mem' := _, zero_mem' := _, neg_mem' := _}

source

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

subgroup G

A nonempty idempotent subset of a finite group is a subgroup

Equations

subgroup_of_idempotent S hS1 hS2 = {carrier := S, mul_mem' := _, one_mem' := _, inv_mem' := _}

source

@[simp]

theorem smul_card_add_subgroup_coe {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS : S.nonempty) :

↑(smul_card_add_subgroup S hS) = fintype.card G • S

source

def smul_card_add_subgroup {G : Type u_1} [add_group G] [fintype G] (S : set G) (hS : S.nonempty) :

add_subgroup G

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

Equations

smul_card_add_subgroup S hS = have one_mem : 0 ∈ fintype.card G • S, from _, add_subgroup_of_idempotent (fintype.card G • S) _ _

source

@[simp]

theorem pow_card_subgroup_coe {G : Type u_1} [group G] [fintype G] (S : set G) (hS : S.nonempty) :

↑(pow_card_subgroup S hS) = S ^ fintype.card G

source

def pow_card_subgroup {G : Type u_1} [group G] [fintype G] (S : set G) (hS : S.nonempty) :

subgroup G

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

Equations

pow_card_subgroup S hS = have one_mem : 1 ∈ S ^ fintype.card G, from _, subgroup_of_idempotent (S ^ fintype.card G) _ _

source

theorem order_of_abs_ne_one {G : Type u} {x : G} [linear_ordered_ring G] (h : |x| ≠ 1) :

order_of x = 0

source

theorem linear_ordered_ring.order_of_le_two {G : Type u} {x : G} [linear_ordered_ring G] :

order_of x ≤ 2

mathlib documentation

Order of an element #

Main definitions #

Tags #