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} [AddMonoid G] {n : ℕ} (x : G) : Function.IsPeriodicPt ((fun x x_1 => x + x_1) x) n 0 ↔ n • x = 0

theorem isPeriodicPt_mul_iff_pow_eq_one {G : Type u_1} [Monoid G] {n : ℕ} (x : G) : Function.IsPeriodicPt ((fun x x_1 => x * x_1) x) n 1 ↔ x ^ n = 1

def IsOfFinAddOrder {G : Type u_1} [AddMonoid G] (x : G) : Prop

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

• IsOfFinAddOrder x = (0 ∈ Function.periodicPts ((fun x x_1 => x + x_1) x))

def IsOfFinOrder {G : Type u_1} [Monoid G] (x : G) : Prop

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

• IsOfFinOrder x = (1 ∈ Function.periodicPts ((fun x x_1 => x * x_1) x))

theorem isOfFinAddOrder_ofMul_iff {G : Type u_1} [Monoid G] {x : G} : IsOfFinAddOrder (↑Additive.ofMul x) ↔ IsOfFinOrder x

theorem isOfFinOrder_ofAdd_iff {A : Type u_3} [AddMonoid A] {a : A} : IsOfFinOrder (↑Multiplicative.ofAdd a) ↔ IsOfFinAddOrder a

theorem isOfFinAddOrder_iff_nsmul_eq_zero {G : Type u_1} [AddMonoid G] (x : G) : IsOfFinAddOrder x ↔ ∃ n, 0 < n ∧ n • x = 0

theorem isOfFinOrder_iff_pow_eq_one {G : Type u_1} [Monoid G] (x : G) : IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1

theorem not_isOfFinAddOrder_of_injective_nsmul {G : Type u_1} [AddMonoid G] {x : G} (h : Function.Injective fun n => n • x) : ¬IsOfFinAddOrder x

See also injective_nsmul_iff_not_isOfFinAddOrder.

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

See also injective_pow_iff_not_isOfFinOrder.

theorem isOfFinAddOrder_iff_coe {G : Type u_1} [AddMonoid G] (H : AddSubmonoid G) (x : { x // x ∈ H }) : IsOfFinAddOrder x ↔ IsOfFinAddOrder ↑x

Elements of finite order are of finite order in submonoids.

theorem isOfFinOrder_iff_coe {G : Type u_1} [Monoid G] (H : Submonoid G) (x : { x // x ∈ H }) : IsOfFinOrder x ↔ IsOfFinOrder ↑x

Elements of finite order are of finite order in submonoids.

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

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

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

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

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

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

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

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

theorem isOfFinAddOrder_zero {G : Type u_1} [AddMonoid G] : IsOfFinAddOrder 0

0 is of finite order in any additive monoid.

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

1 is of finite order in any monoid.

theorem IsOfFinAddOrder.addGroupMultiples.proof_1 {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) : ∃ n, 0 < n ∧ n • x = 0

noncomputable abbrev IsOfFinAddOrder.addGroupMultiples {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) : AddGroup { x // x ∈ AddSubmonoid.multiples x }

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

Equations

• One or more equations did not get rendered due to their size.

theorem IsOfFinAddOrder.addGroupMultiples.proof_2 {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) : 0 < Exists.choose (_ : ∃ n, 0 < n ∧ n • x = 0) ∧ Exists.choose (_ : ∃ n, 0 < n ∧ n • x = 0) • x = 0

@[inline, reducible]

noncomputable abbrev IsOfFinOrder.groupPowers {G : Type u_1} [Monoid G] {x : G} (hx : IsOfFinOrder x) : Group { x // x ∈ Submonoid.powers x }

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def addOrderOf {G : Type u_1} [AddMonoid G] (x : G) : ℕ

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

Equations

• addOrderOf x = Function.minimalPeriod (fun x => x + x) 0

noncomputable def orderOf {G : Type u_1} [Monoid G] (x : G) : ℕ

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

Equations

• orderOf x = Function.minimalPeriod (fun x => x * x) 1

@[simp]

theorem addOrderOf_ofMul_eq_orderOf {G : Type u_1} [Monoid G] (x : G) : addOrderOf (↑Additive.ofMul x) = orderOf x

@[simp]

theorem orderOf_ofAdd_eq_addOrderOf {A : Type u_3} [AddMonoid A] (a : A) : orderOf (↑Multiplicative.ofAdd a) = addOrderOf a

theorem addOrderOf_pos' {G : Type u_1} [AddMonoid G] {x : G} (h : IsOfFinAddOrder x) : 0 < addOrderOf x

theorem orderOf_pos' {G : Type u_1} [Monoid G] {x : G} (h : IsOfFinOrder x) : 0 < orderOf x

theorem addOrderOf_nsmul_eq_zero {G : Type u_1} [AddMonoid G] (x : G) : addOrderOf x • x = 0

theorem pow_orderOf_eq_one {G : Type u_1} [Monoid G] (x : G) : x ^ orderOf x = 1

theorem addOrderOf_eq_zero {G : Type u_1} [AddMonoid G] {x : G} (h : ¬IsOfFinAddOrder x) : addOrderOf x = 0

theorem orderOf_eq_zero {G : Type u_1} [Monoid G] {x : G} (h : ¬IsOfFinOrder x) : orderOf x = 0

theorem addOrderOf_eq_zero_iff {G : Type u_1} [AddMonoid G] {x : G} : addOrderOf x = 0 ↔ ¬IsOfFinAddOrder x

theorem orderOf_eq_zero_iff {G : Type u_1} [Monoid G] {x : G} : orderOf x = 0 ↔ ¬IsOfFinOrder x

theorem addOrderOf_eq_zero_iff' {G : Type u_1} [AddMonoid G] {x : G} : addOrderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → n • x ≠ 0

theorem orderOf_eq_zero_iff' {G : Type u_1} [Monoid G] {x : G} : orderOf x = 0 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

theorem addOrderOf_eq_iff {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (h : 0 < n) : addOrderOf x = n ↔ n • x = 0 ∧ ∀ (m : ℕ), m < n → 0 < m → m • x ≠ 0

theorem orderOf_eq_iff {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (h : 0 < n) : orderOf x = n ↔ x ^ n = 1 ∧ ∀ (m : ℕ), m < n → 0 < m → x ^ m ≠ 1

theorem addOrderOf_pos_iff {G : Type u_1} [AddMonoid G] {x : G} : 0 < addOrderOf x ↔ IsOfFinAddOrder x

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

theorem orderOf_pos_iff {G : Type u_1} [Monoid G] {x : G} : 0 < orderOf x ↔ IsOfFinOrder x

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

theorem IsOfFinAddOrder.mono {G : Type u_1} {β : Type u_5} [AddMonoid G] {x : G} [AddMonoid β] {y : β} (hx : IsOfFinAddOrder x) (h : addOrderOf y ∣ addOrderOf x) : IsOfFinAddOrder y

theorem IsOfFinOrder.mono {G : Type u_1} {β : Type u_5} [Monoid G] {x : G} [Monoid β] {y : β} (hx : IsOfFinOrder x) (h : orderOf y ∣ orderOf x) : IsOfFinOrder y

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

theorem pow_ne_one_of_lt_orderOf' {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (n0 : n ≠ 0) (h : n < orderOf x) : x ^ n ≠ 1

theorem addOrderOf_le_of_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (hn : 0 < n) (h : n • x = 0) : addOrderOf x ≤ n

theorem orderOf_le_of_pow_eq_one {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (hn : 0 < n) (h : x ^ n = 1) : orderOf x ≤ n

@[simp]

theorem addOrderOf_zero {G : Type u_1} [AddMonoid G] : addOrderOf 0 = 1

@[simp]

theorem orderOf_one {G : Type u_1} [Monoid G] : orderOf 1 = 1

@[simp]

theorem AddMonoid.addOrderOf_eq_one_iff {G : Type u_1} [AddMonoid G] {x : G} : addOrderOf x = 1 ↔ x = 0

@[simp]

theorem orderOf_eq_one_iff {G : Type u_1} [Monoid G] {x : G} : orderOf x = 1 ↔ x = 1

theorem nsmul_eq_mod_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} : n • x = (n % addOrderOf x) • x

theorem pow_eq_mod_orderOf {G : Type u_1} [Monoid G] {x : G} {n : ℕ} : x ^ n = x ^ (n % orderOf x)

theorem addOrderOf_dvd_of_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (h : n • x = 0) : addOrderOf x ∣ n

theorem orderOf_dvd_of_pow_eq_one {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (h : x ^ n = 1) : orderOf x ∣ n

theorem addOrderOf_dvd_iff_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} : addOrderOf x ∣ n ↔ n • x = 0

theorem orderOf_dvd_iff_pow_eq_one {G : Type u_1} [Monoid G] {x : G} {n : ℕ} : orderOf x ∣ n ↔ x ^ n = 1

theorem addOrderOf_smul_dvd {G : Type u_1} [AddMonoid G] {x : G} (n : ℕ) : addOrderOf (n • x) ∣ addOrderOf x

theorem orderOf_pow_dvd {G : Type u_1} [Monoid G] {x : G} (n : ℕ) : orderOf (x ^ n) ∣ orderOf x

theorem nsmul_injective_of_lt_addOrderOf {G : Type u_1} [AddMonoid G] {n : ℕ} {m : ℕ} (x : G) (hn : n < addOrderOf x) (hm : m < addOrderOf x) (eq : n • x = m • x) : n = m

theorem pow_injective_of_lt_orderOf {G : Type u_1} [Monoid G] {n : ℕ} {m : ℕ} (x : G) (hn : n < orderOf x) (hm : m < orderOf x) (eq : x ^ n = x ^ m) : n = m

theorem mem_multiples_iff_mem_range_addOrderOf' {G : Type u_1} [AddMonoid G] {x : G} {y : G} [DecidableEq G] (hx : 0 < addOrderOf x) : y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun x => x • x) (Finset.range (addOrderOf x))

theorem mem_powers_iff_mem_range_order_of' {G : Type u_1} [Monoid G] {x : G} {y : G} [DecidableEq G] (hx : 0 < orderOf x) : y ∈ Submonoid.powers x ↔ y ∈ Finset.image (fun x => x ^ x) (Finset.range (orderOf x))

theorem nsmul_eq_zero_iff_modEq {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} : n • x = 0 ↔ n ≡ 0 [MOD addOrderOf x]

theorem pow_eq_one_iff_modEq {G : Type u_1} [Monoid G] {x : G} {n : ℕ} : x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

theorem addOrderOf_map_dvd {G : Type u_1} [AddMonoid G] {H : Type u_6} [AddMonoid H] (ψ : G →+ H) (x : G) : addOrderOf (↑ψ x) ∣ addOrderOf x

theorem orderOf_map_dvd {G : Type u_1} [Monoid G] {H : Type u_6} [Monoid H] (ψ : G →* H) (x : G) : orderOf (↑ψ x) ∣ orderOf x

theorem exists_nsmul_eq_self_of_coprime {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (h : Nat.Coprime n (addOrderOf x)) : ∃ m, m • n • x = x

theorem exists_pow_eq_self_of_coprime {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (h : Nat.Coprime n (orderOf x)) : ∃ m, (x ^ n) ^ m = x

theorem addOrderOf_eq_of_nsmul_and_div_prime_nsmul {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (hn : 0 < n) (hx : n • x = 0) (hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → (n / p) • x ≠ 0) : addOrderOf x = 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} [Monoid G] {x : G} {n : ℕ} (hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ (p : ℕ), Nat.Prime p → p ∣ n → x ^ (n / p) ≠ 1) : orderOf x = 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} [AddMonoid G] {x : G} {H : Type u_6} [AddMonoid H] {y : H} : addOrderOf x = addOrderOf y ↔ ∀ (n : ℕ), n • x = 0 ↔ n • y = 0

theorem orderOf_eq_orderOf_iff {G : Type u_1} [Monoid G] {x : G} {H : Type u_6} [Monoid H] {y : H} : orderOf x = orderOf y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1

theorem addOrderOf_injective {G : Type u_1} [AddMonoid G] {H : Type u_6} [AddMonoid H] (f : G →+ H) (hf : Function.Injective ↑f) (x : G) : addOrderOf (↑f x) = addOrderOf x

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

@[simp]

theorem addOrderOf_addSubmonoid {G : Type u_1} [AddMonoid G] {H : AddSubmonoid G} (y : { x // x ∈ H }) : addOrderOf ↑y = addOrderOf y

@[simp]

theorem orderOf_submonoid {G : Type u_1} [Monoid G] {H : Submonoid G} (y : { x // x ∈ H }) : orderOf ↑y = orderOf y

theorem addOrderOf_addUnits {G : Type u_1} [AddMonoid G] {y : AddUnits G} : addOrderOf ↑y = addOrderOf y

theorem orderOf_units {G : Type u_1} [Monoid G] {y : Gˣ} : orderOf ↑y = orderOf y

theorem addOrderOf_nsmul' {G : Type u_1} [AddMonoid G] (x : G) {n : ℕ} (h : n ≠ 0) : addOrderOf (n • x) = addOrderOf x / Nat.gcd (addOrderOf x) n

theorem orderOf_pow' {G : Type u_1} [Monoid G] (x : G) {n : ℕ} (h : n ≠ 0) : orderOf (x ^ n) = orderOf x / Nat.gcd (orderOf x) n

theorem addOrderOf_nsmul'' {G : Type u_1} [AddMonoid G] (x : G) (n : ℕ) (h : IsOfFinAddOrder x) : addOrderOf (n • x) = addOrderOf x / Nat.gcd (addOrderOf x) n

theorem orderOf_pow'' {G : Type u_1} [Monoid G] (x : G) (n : ℕ) (h : IsOfFinOrder x) : orderOf (x ^ n) = orderOf x / Nat.gcd (orderOf x) n

theorem addOrderOf_nsmul_coprime {G : Type u_1} [AddMonoid G] {y : G} {m : ℕ} (h : Nat.Coprime (addOrderOf y) m) : addOrderOf (m • y) = addOrderOf y

theorem orderOf_pow_coprime {G : Type u_1} [Monoid G] {y : G} {m : ℕ} (h : Nat.Coprime (orderOf y) m) : orderOf (y ^ m) = orderOf y

theorem AddCommute.addOrderOf_add_dvd_lcm {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) : addOrderOf (x + y) ∣ Nat.lcm (addOrderOf x) (addOrderOf y)

theorem Commute.orderOf_mul_dvd_lcm {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) : orderOf (x * y) ∣ Nat.lcm (orderOf x) (orderOf y)

theorem AddCommute.addOrderOf_dvd_lcm_add {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) : addOrderOf y ∣ Nat.lcm (addOrderOf x) (addOrderOf (x + y))

theorem Commute.orderOf_dvd_lcm_mul {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) : orderOf y ∣ Nat.lcm (orderOf x) (orderOf (x * y))

theorem AddCommute.addOrderOf_add_dvd_mul_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) : addOrderOf (x + y) ∣ addOrderOf x * addOrderOf y

theorem Commute.orderOf_mul_dvd_mul_orderOf {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) : orderOf (x * y) ∣ orderOf x * orderOf y

theorem AddCommute.addOrderOf_add_eq_mul_addOrderOf_of_coprime {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) (hco : Nat.Coprime (addOrderOf x) (addOrderOf y)) : addOrderOf (x + y) = addOrderOf x * addOrderOf y

theorem Commute.orderOf_mul_eq_mul_orderOf_of_coprime {G : Type u_1} [Monoid G] {x : G} {y : G} (h : Commute x y) (hco : Nat.Coprime (orderOf x) (orderOf y)) : orderOf (x * y) = orderOf x * orderOf y

theorem AddCommute.isOfFinAddOrder_add {G : Type u_1} [AddMonoid G] {x : G} {y : G} (h : AddCommute x y) (hx : IsOfFinAddOrder x) (hy : IsOfFinAddOrder y) : IsOfFinAddOrder (x + y)

Commuting elements of finite additive order are closed under addition.

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

Commuting elements of finite order are closed under multiplication.

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

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

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

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

theorem addOrderOf_eq_prime {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] (hg : p • x = 0) (hg1 : x ≠ 0) : addOrderOf x = p

theorem orderOf_eq_prime {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] (hg : x ^ p = 1) (hg1 : x ≠ 1) : orderOf x = p

theorem addOrderOf_eq_prime_pow {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} {p : ℕ} [hp : Fact (Nat.Prime p)] (hnot : ¬p ^ n • x = 0) (hfin : p ^ (n + 1) • x = 0) : addOrderOf x = p ^ (n + 1)

theorem orderOf_eq_prime_pow {G : Type u_1} [Monoid G] {x : G} {n : ℕ} {p : ℕ} [hp : Fact (Nat.Prime p)] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) : orderOf x = p ^ (n + 1)

abbrev exists_addOrderOf_eq_prime_pow_iff.match_1 {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} (motive : (∃ k, addOrderOf x = p ^ k) → Prop) : (x : ∃ k, addOrderOf x = p ^ k) → ((k : ℕ) → (hk : addOrderOf x = p ^ k) → motive (_ : ∃ k, addOrderOf x = p ^ k)) → motive x

Equations

• exists_addOrderOf_eq_prime_pow_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

abbrev exists_addOrderOf_eq_prime_pow_iff.match_2 {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} (motive : (∃ m, p ^ m • x = 0) → Prop) : (x : ∃ m, p ^ m • x = 0) → ((w : ℕ) → (hm : p ^ w • x = 0) → motive (_ : ∃ m, p ^ m • x = 0)) → motive x

Equations

• exists_addOrderOf_eq_prime_pow_iff.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem exists_addOrderOf_eq_prime_pow_iff {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : (∃ k, addOrderOf x = p ^ k) ↔ ∃ m, p ^ m • x = 0

theorem exists_orderOf_eq_prime_pow_iff {G : Type u_1} [Monoid G] {x : G} {p : ℕ} [hp : Fact (Nat.Prime p)] : (∃ k, orderOf x = p ^ k) ↔ ∃ m, x ^ p ^ m = 1

theorem nsmul_eq_nsmul_iff_modEq {G : Type u_1} [AddLeftCancelMonoid G] (x : G) {m : ℕ} {n : ℕ} : n • x = m • x ↔ n ≡ m [MOD addOrderOf x]

theorem pow_eq_pow_iff_modEq {G : Type u_1} [LeftCancelMonoid G] (x : G) {m : ℕ} {n : ℕ} : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

@[simp]

theorem injective_nsmul_iff_not_isOfFinAddOrder {G : Type u_1} [AddLeftCancelMonoid G] {x : G} : (Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x

@[simp]

theorem injective_pow_iff_not_isOfFinOrder {G : Type u_1} [LeftCancelMonoid G] {x : G} : (Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x

theorem nsmul_inj_mod {G : Type u_1} [AddLeftCancelMonoid G] (x : G) {n : ℕ} {m : ℕ} : n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x

theorem pow_inj_mod {G : Type u_1} [LeftCancelMonoid G] (x : G) {n : ℕ} {m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x

theorem nsmul_inj_iff_of_addOrderOf_eq_zero {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (h : addOrderOf x = 0) {n : ℕ} {m : ℕ} : n • x = m • x ↔ n = m

theorem pow_inj_iff_of_orderOf_eq_zero {G : Type u_1} [LeftCancelMonoid G] (x : G) (h : orderOf x = 0) {n : ℕ} {m : ℕ} : x ^ n = x ^ m ↔ n = m

theorem infinite_not_isOfFinAddOrder {G : Type u_1} [AddLeftCancelMonoid G] {x : G} (h : ¬IsOfFinAddOrder x) : Set.Infinite {y | ¬IsOfFinAddOrder y}

theorem infinite_not_isOfFinOrder {G : Type u_1} [LeftCancelMonoid G] {x : G} (h : ¬IsOfFinOrder x) : Set.Infinite {y | ¬IsOfFinOrder y}

theorem IsOfFinAddOrder.neg {G : Type u_1} [AddGroup G] {x : G} (hx : IsOfFinAddOrder x) : IsOfFinAddOrder (-x)

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

theorem IsOfFinOrder.inv {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) : IsOfFinOrder x⁻¹

Inverses of elements of finite order have finite order.

@[simp]

theorem isOfFinAddOrder_neg_iff {G : Type u_1} [AddGroup G] {x : G} : IsOfFinAddOrder (-x) ↔ IsOfFinAddOrder x

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

@[simp]

theorem isOfFinOrder_inv_iff {G : Type u_1} [Group G] {x : G} : IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x

Inverses of elements of finite order have finite order.

theorem addOrderOf_dvd_iff_zsmul_eq_zero {G : Type u_1} [AddGroup G] {x : G} {i : ℤ} : ↑(addOrderOf x) ∣ i ↔ i • x = 0

theorem orderOf_dvd_iff_zpow_eq_one {G : Type u_1} [Group G] {x : G} {i : ℤ} : ↑(orderOf x) ∣ i ↔ x ^ i = 1

@[simp]

theorem addOrderOf_neg {G : Type u_1} [AddGroup G] (x : G) : addOrderOf (-x) = addOrderOf x

@[simp]

theorem orderOf_inv {G : Type u_1} [Group G] (x : G) : orderOf x⁻¹ = orderOf x

theorem addOrderOf_addSubgroup {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (y : { x // x ∈ H }) : addOrderOf ↑y = addOrderOf y

theorem orderOf_subgroup {G : Type u_1} [Group G] {H : Subgroup G} (y : { x // x ∈ H }) : orderOf ↑y = orderOf y

theorem zsmul_eq_mod_addOrderOf {G : Type u_1} [AddGroup G] {x : G} {i : ℤ} : i • x = (i % ↑(addOrderOf x)) • x

theorem zpow_eq_mod_orderOf {G : Type u_1} [Group G] {x : G} {i : ℤ} : x ^ i = x ^ (i % ↑(orderOf x))

@[simp]

theorem zsmul_smul_addOrderOf {G : Type u_1} [AddGroup G] {x : G} {i : ℤ} : addOrderOf x • i • x = 0

@[simp]

theorem zpow_pow_orderOf {G : Type u_1} [Group G] {x : G} {i : ℤ} : (x ^ i) ^ orderOf x = 1

theorem IsOfFinAddOrder.zsmul {G : Type u_1} [AddGroup G] {x : G} (h : IsOfFinAddOrder x) {i : ℤ} : IsOfFinAddOrder (i • x)

theorem IsOfFinOrder.zpow {G : Type u_1} [Group G] {x : G} (h : IsOfFinOrder x) {i : ℤ} : IsOfFinOrder (x ^ i)

theorem IsOfFinAddOrder.of_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {y : G} (h : IsOfFinAddOrder x) (h' : y ∈ AddSubgroup.zmultiples x) : IsOfFinAddOrder y

theorem IsOfFinOrder.of_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} (h : IsOfFinOrder x) (h' : y ∈ Subgroup.zpowers x) : IsOfFinOrder y

theorem addOrderOf_dvd_of_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {y : G} (h : y ∈ AddSubgroup.zmultiples x) : addOrderOf y ∣ addOrderOf x

theorem orderOf_dvd_of_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} (h : y ∈ Subgroup.zpowers x) : orderOf y ∣ orderOf x

theorem smul_eq_self_of_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} {α : Type u_6} [MulAction G α] (hx : x ∈ Subgroup.zpowers y) {a : α} (hs : y • a = a) : x • a = a

theorem vadd_eq_self_of_mem_zmultiples {α : Type u_6} {G : Type u_7} [AddGroup G] [AddAction G α] {x : G} {y : G} (hx : x ∈ AddSubgroup.zmultiples y) {a : α} (hs : y +ᵥ a = a) : x +ᵥ a = a

theorem IsOfFinAddOrder.add {G : Type u_1} [AddCommMonoid G] {x : G} {y : G} (hx : IsOfFinAddOrder x) (hy : IsOfFinAddOrder y) : IsOfFinAddOrder (x + y)

Elements of finite additive order are closed under addition.

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

Elements of finite order are closed under multiplication.

theorem sum_card_addOrderOf_eq_card_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {n : ℕ} [Fintype G] [DecidableEq G] (hn : n ≠ 0) : (Finset.sum (Finset.filter (fun x => x ∣ n) (Finset.range (Nat.succ n))) fun m => Finset.card (Finset.filter (fun x => addOrderOf x = m) Finset.univ)) = Finset.card (Finset.filter (fun x => n • x = 0) Finset.univ)

abbrev sum_card_addOrderOf_eq_card_nsmul_eq_zero.match_1 {G : Type u_1} [AddMonoid G] {n : ℕ} (x : G) (motive : addOrderOf x ∣ n → Prop) : (x : addOrderOf x ∣ n) → ((m : ℕ) → (hm : n = addOrderOf x * m) → motive (_ : ∃ c, n = addOrderOf x * c)) → motive x

Equations

• sum_card_addOrderOf_eq_card_nsmul_eq_zero.match_1 x motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem sum_card_orderOf_eq_card_pow_eq_one {G : Type u_1} [Monoid G] {n : ℕ} [Fintype G] [DecidableEq G] (hn : n ≠ 0) : (Finset.sum (Finset.filter (fun x => x ∣ n) (Finset.range (Nat.succ n))) fun m => Finset.card (Finset.filter (fun x => orderOf x = m) Finset.univ)) = Finset.card (Finset.filter (fun x => x ^ n = 1) Finset.univ)

theorem addOrderOf_le_card_univ {G : Type u_1} [AddMonoid G] {x : G} [Fintype G] : addOrderOf x ≤ Fintype.card G

theorem orderOf_le_card_univ {G : Type u_1} [Monoid G] {x : G} [Fintype G] : orderOf x ≤ Fintype.card G

theorem exists_nsmul_eq_zero {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) : IsOfFinAddOrder x

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

theorem addOrderOf_pos {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) : 0 < addOrderOf x

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

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

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

theorem addOrderOf_nsmul {G : Type u_1} [AddLeftCancelMonoid G] {n : ℕ} [Finite G] (x : G) : addOrderOf (n • x) = addOrderOf x / Nat.gcd (addOrderOf x) 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} [LeftCancelMonoid G] {n : ℕ} [Finite G] (x : G) : orderOf (x ^ n) = orderOf x / Nat.gcd (orderOf x) 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} [AddLeftCancelMonoid G] {x : G} {y : G} [Finite G] [DecidableEq G] : y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image ((fun x x_1 => x_1 • x) x) (Finset.range (addOrderOf x))

theorem mem_powers_iff_mem_range_orderOf {G : Type u_1} [LeftCancelMonoid G] {x : G} {y : G} [Finite G] [DecidableEq G] : y ∈ Submonoid.powers x ↔ y ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (orderOf x))

noncomputable instance decidableMultiples {G : Type u_1} [AddLeftCancelMonoid G] {x : G} : DecidablePred fun x => x ∈ AddSubmonoid.multiples x

Equations

• decidableMultiples = Classical.decPred fun x => x ∈ AddSubmonoid.multiples x

noncomputable instance decidablePowers {G : Type u_1} [LeftCancelMonoid G] {x : G} : DecidablePred fun x => x ∈ Submonoid.powers x

Equations

• decidablePowers = Classical.decPred fun x => x ∈ Submonoid.powers x

theorem finEquivMultiples.proof_1 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (n : Fin (addOrderOf x)) : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x

abbrev finEquivMultiples.match_1 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) : ∀ (val : ℕ) (h₁ : val < addOrderOf x) (motive : (x : Fin (addOrderOf x)) → (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) { val := val, isLt := h₁ } = (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) x → Prop) (x : Fin (addOrderOf x)) (ij : (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) { val := val, isLt := h₁ } = (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) x), (∀ (val_1 : ℕ) (h₂ : val_1 < addOrderOf x) (ij : (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) { val := val, isLt := h₁ } = (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) { val := val_1, isLt := h₂ }), motive { val := val_1, isLt := h₂ } ij) → motive x ij

Equations

• One or more equations did not get rendered due to their size.

abbrev finEquivMultiples.match_2 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) : ∀ (x : Fin (addOrderOf x)) (motive : (x_1 : Fin (addOrderOf x)) → (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_2 => x_2 • x) x y = ↑n • x) }) x_1 = (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_2 => x_2 • x) x y = ↑n • x) }) x → Prop) (x_1 : Fin (addOrderOf x)) (ij : (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_2 => x_2 • x) x y = ↑n • x) }) x_1 = (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_2 => x_2 • x) x y = ↑n • x) }) x), (∀ (val : ℕ) (h₁ : val < addOrderOf x) (ij : (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_2 => x_2 • x) x y = ↑n • x) }) { val := val, isLt := h₁ } = (fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_2 => x_2 • x) x y = ↑n • x) }) x), motive { val := val, isLt := h₁ } ij) → motive x_1 ij

Equations

• One or more equations did not get rendered due to their size.

abbrev finEquivMultiples.match_3 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (motive : ↑↑(AddSubmonoid.multiples x) → Prop) : (x : ↑↑(AddSubmonoid.multiples x)) → ((i : ℕ) → motive { val := (fun x x_1 => x_1 • x) x i, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = (fun x x_1 => x_1 • x) x i) }) → motive x

Equations

• One or more equations did not get rendered due to their size.

theorem finEquivMultiples.proof_2 {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) : (Function.Injective fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }) ∧ Function.Surjective fun n => { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }

noncomputable def finEquivMultiples {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) : Fin (addOrderOf x) ≃ ↑↑(AddSubmonoid.multiples x)

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

Equations

• One or more equations did not get rendered due to their size.

noncomputable def finEquivPowers {G : Type u_1} [LeftCancelMonoid G] [Finite G] (x : G) : Fin (orderOf x) ≃ ↑↑(Submonoid.powers x)

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem finEquivMultiples_apply {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {x : G} {n : Fin (addOrderOf x)} : ↑(finEquivMultiples x) n = { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }

@[simp]

theorem finEquivPowers_apply {G : Type u_1} [LeftCancelMonoid G] [Finite G] {x : G} {n : Fin (orderOf x)} : ↑(finEquivPowers x) n = { val := x ^ ↑n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ ↑n) }

@[simp]

theorem finEquivMultiples_symm_apply {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) (n : ℕ) {hn : ∃ m, m • x = n • x} : ↑(finEquivMultiples x).symm { val := n • x, property := hn } = { val := n % addOrderOf x, isLt := (_ : n % addOrderOf x < addOrderOf x) }

@[simp]

theorem finEquivPowers_symm_apply {G : Type u_1} [LeftCancelMonoid G] [Finite G] (x : G) (n : ℕ) {hn : ∃ m, x ^ m = x ^ n} : ↑(finEquivPowers x).symm { val := x ^ n, property := hn } = { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }

noncomputable def multiplesEquivMultiples {G : Type u_1} [AddLeftCancelMonoid G] {x : G} {y : G} [Finite G] (h : addOrderOf x = addOrderOf y) : ↑↑(AddSubmonoid.multiples x) ≃ ↑↑(AddSubmonoid.multiples y)

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

Equations

• multiplesEquivMultiples h = (finEquivMultiples x).symm.trans ((Fin.castIso h).trans (finEquivMultiples y))

noncomputable def powersEquivPowers {G : Type u_1} [LeftCancelMonoid G] {x : G} {y : G} [Finite G] (h : orderOf x = orderOf 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

• powersEquivPowers h = (finEquivPowers x).symm.trans ((Fin.castIso h).trans (finEquivPowers y))

@[simp]

theorem multiplesEquivMultiples_apply {G : Type u_1} [AddLeftCancelMonoid G] {x : G} {y : G} [Finite G] (h : addOrderOf x = addOrderOf y) (n : ℕ) : ↑(multiplesEquivMultiples h) { val := n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = n • x) } = { val := n • y, property := (_ : ∃ y, (fun x x_1 => x_1 • x) y y = n • y) }

@[simp]

theorem powersEquivPowers_apply {G : Type u_1} [LeftCancelMonoid G] {x : G} {y : G} [Finite G] (h : orderOf x = orderOf y) (n : ℕ) : ↑(powersEquivPowers h) { val := x ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ n) } = { val := y ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) y y = y ^ n) }

noncomputable instance instFintypeSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidPowers {G : Type u_1} [AddLeftCancelMonoid G] {x : G} [Fintype G] : Fintype { x // x ∈ AddSubmonoid.multiples x }

Equations

• instFintypeSubtypeMemAddSubmonoidToAddZeroClassToAddMonoidInstMembershipInstSetLikeAddSubmonoidPowers = inferInstanceAs (Fintype { y // y ∈ AddSubmonoid.multiples x })

noncomputable instance instFintypeSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidPowers {G : Type u_1} [LeftCancelMonoid G] {x : G} [Fintype G] : Fintype { x // x ∈ Submonoid.powers x }

Equations

• instFintypeSubtypeMemSubmonoidToMulOneClassToMonoidInstMembershipInstSetLikeSubmonoidPowers = inferInstanceAs (Fintype { y // y ∈ Submonoid.powers x })

theorem addOrderOf_eq_card_multiples {G : Type u_1} [AddLeftCancelMonoid G] {x : G} [Fintype G] : addOrderOf x = Fintype.card ↑↑(AddSubmonoid.multiples x)

theorem orderOf_eq_card_powers {G : Type u_1} [LeftCancelMonoid G] {x : G} [Fintype G] : orderOf x = Fintype.card ↑↑(Submonoid.powers x)

theorem exists_zsmul_eq_zero {G : Type u_1} [AddGroup G] [Finite G] (x : G) : ∃ i x, i • x = 0

theorem exists_zpow_eq_one {G : Type u_1} [Group G] [Finite G] (x : G) : ∃ i x, x ^ i = 1

abbrev mem_multiples_iff_mem_zmultiples.match_2 {G : Type u_1} [AddGroup G] {x : G} {y : G} (motive : y ∈ AddSubgroup.zmultiples x → Prop) : (x : y ∈ AddSubgroup.zmultiples x) → ((i : ℤ) → (hi : (fun x x_1 => x_1 • x) x i = y) → motive (_ : ∃ y, (fun x x_1 => x_1 • x) x y = y)) → motive x

Equations

• mem_multiples_iff_mem_zmultiples.match_2 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

abbrev mem_multiples_iff_mem_zmultiples.match_1 {G : Type u_1} [AddGroup G] {x : G} {y : G} (motive : y ∈ AddSubmonoid.multiples x → Prop) : (x : y ∈ AddSubmonoid.multiples x) → ((n : ℕ) → (hn : (fun x x_1 => x_1 • x) x n = y) → motive (_ : ∃ y, (fun x x_1 => x_1 • x) x y = y)) → motive x

Equations

• mem_multiples_iff_mem_zmultiples.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem mem_multiples_iff_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {y : G} [Finite G] : y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x

theorem mem_powers_iff_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} [Finite G] : y ∈ Submonoid.powers x ↔ y ∈ Subgroup.zpowers x

theorem multiples_eq_zmultiples {G : Type u_1} [AddGroup G] [Finite G] (x : G) : ↑(AddSubmonoid.multiples x) = ↑(AddSubgroup.zmultiples x)

theorem powers_eq_zpowers {G : Type u_1} [Group G] [Finite G] (x : G) : ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)

theorem mem_zmultiples_iff_mem_range_addOrderOf {G : Type u_1} [AddGroup G] {x : G} {y : G} [Finite G] [DecidableEq G] : y ∈ AddSubgroup.zmultiples x ↔ y ∈ Finset.image ((fun x x_1 => x_1 • x) x) (Finset.range (addOrderOf x))

theorem mem_zpowers_iff_mem_range_orderOf {G : Type u_1} [Group G] {x : G} {y : G} [Finite G] [DecidableEq G] : y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image ((fun x x_1 => x ^ x_1) x) (Finset.range (orderOf x))

theorem zsmul_eq_zero_iff_modEq {G : Type u_1} [AddGroup G] {x : G} {n : ℤ} : n • x = 0 ↔ n ≡ 0 [ZMOD ↑(addOrderOf x)]

theorem zpow_eq_one_iff_modEq {G : Type u_1} [Group G] {x : G} {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]

theorem zsmul_eq_zsmul_iff_modEq {G : Type u_1} [AddGroup G] {x : G} {m : ℤ} {n : ℤ} : m • x = n • x ↔ m ≡ n [ZMOD ↑(addOrderOf x)]

theorem zpow_eq_zpow_iff_modEq {G : Type u_1} [Group G] {x : G} {m : ℤ} {n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD ↑(orderOf x)]

@[simp]

theorem injective_zsmul_iff_not_isOfFinAddOrder {G : Type u_1} [AddGroup G] {x : G} : (Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x

@[simp]

theorem injective_zpow_iff_not_isOfFinOrder {G : Type u_1} [Group G] {x : G} : (Function.Injective fun n => x ^ n) ↔ ¬IsOfFinOrder x

noncomputable instance decidableZmultiples {G : Type u_1} [AddGroup G] {x : G} : DecidablePred fun x => x ∈ AddSubgroup.zmultiples x

Equations

• decidableZmultiples = Classical.decPred fun x => x ∈ AddSubgroup.zmultiples x

noncomputable instance decidableZpowers {G : Type u_1} [Group G] {x : G} : DecidablePred fun x => x ∈ Subgroup.zpowers x

Equations

• decidableZpowers = Classical.decPred fun x => x ∈ Subgroup.zpowers x

noncomputable def finEquivZmultiples {G : Type u_1} [AddGroup G] [Finite G] (x : G) : Fin (addOrderOf x) ≃ ↑↑(AddSubgroup.zmultiples x)

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

Equations

• finEquivZmultiples x = (finEquivMultiples x).trans (Equiv.Set.ofEq (_ : ↑(AddSubmonoid.multiples x) = ↑(AddSubgroup.zmultiples x)))

noncomputable def finEquivZpowers {G : Type u_1} [Group G] [Finite G] (x : G) : Fin (orderOf x) ≃ ↑↑(Subgroup.zpowers x)

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

Equations

• finEquivZpowers x = (finEquivPowers x).trans (Equiv.Set.ofEq (_ : ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)))

@[simp]

theorem finEquivZmultiples_apply {G : Type u_1} [AddGroup G] {x : G} [Finite G] {n : Fin (addOrderOf x)} : ↑(finEquivZmultiples x) n = { val := ↑n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = ↑n • x) }

@[simp]

theorem finEquivZpowers_apply {G : Type u_1} [Group G] {x : G} [Finite G] {n : Fin (orderOf x)} : ↑(finEquivZpowers x) n = { val := x ^ ↑n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ ↑n) }

@[simp]

theorem finEquivZmultiples_symm_apply {G : Type u_1} [AddGroup G] [Finite G] (x : G) (n : ℕ) {hn : ∃ m, m • x = n • x} : ↑(finEquivZmultiples x).symm { val := n • x, property := hn } = { val := n % addOrderOf x, isLt := (_ : n % addOrderOf x < addOrderOf x) }

@[simp]

theorem finEquivZpowers_symm_apply {G : Type u_1} [Group G] [Finite G] (x : G) (n : ℕ) {hn : ∃ m, x ^ m = x ^ n} : ↑(finEquivZpowers x).symm { val := x ^ n, property := hn } = { val := n % orderOf x, isLt := (_ : n % orderOf x < orderOf x) }

noncomputable def zmultiplesEquivZmultiples {G : Type u_1} [AddGroup G] {x : G} {y : G} [Finite G] (h : addOrderOf x = addOrderOf y) : ↑↑(AddSubgroup.zmultiples x) ≃ ↑↑(AddSubgroup.zmultiples y)

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

Equations

• zmultiplesEquivZmultiples h = (finEquivZmultiples x).symm.trans ((Fin.castIso h).trans (finEquivZmultiples y))

noncomputable def zpowersEquivZpowers {G : Type u_1} [Group G] {x : G} {y : G} [Finite G] (h : orderOf x = orderOf 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

• zpowersEquivZpowers h = (finEquivZpowers x).symm.trans ((Fin.castIso h).trans (finEquivZpowers y))

@[simp]

theorem zmultiples_equiv_zmultiples_apply {G : Type u_1} [AddGroup G] {x : G} {y : G} [Finite G] (h : addOrderOf x = addOrderOf y) (n : ℕ) : ↑(zmultiplesEquivZmultiples h) { val := n • x, property := (_ : ∃ y, (fun x x_1 => x_1 • x) x y = n • x) } = { val := n • y, property := (_ : ∃ y, (fun x x_1 => x_1 • x) y y = n • y) }

@[simp]

theorem zpowersEquivZpowers_apply {G : Type u_1} [Group G] {x : G} {y : G} [Finite G] (h : orderOf x = orderOf y) (n : ℕ) : ↑(zpowersEquivZpowers h) { val := x ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) x y = x ^ n) } = { val := y ^ n, property := (_ : ∃ y, (fun x x_1 => x ^ x_1) y y = y ^ n) }

theorem addOrderOf_eq_card_zmultiples {G : Type u_1} [AddGroup G] {x : G} [Fintype G] : addOrderOf x = Fintype.card { x // x ∈ AddSubgroup.zmultiples x }

See also Nat.card_zmultiples'.

theorem orderOf_eq_card_zpowers {G : Type u_1} [Group G] {x : G} [Fintype G] : orderOf x = Fintype.card { x // x ∈ Subgroup.zpowers x }

See also Nat.card_zpowers'.

theorem card_zmultiples_le {G : Type u_1} [AddGroup G] [Fintype G] (a : G) {k : ℕ} (k_pos : k ≠ 0) (ha : k • a = 0) : Fintype.card { x // x ∈ AddSubgroup.zmultiples a } ≤ k

theorem card_zpowers_le {G : Type u_1} [Group G] [Fintype G] (a : G) {k : ℕ} (k_pos : k ≠ 0) (ha : a ^ k = 1) : Fintype.card { x // x ∈ Subgroup.zpowers a } ≤ k

theorem addOrderOf_dvd_card_univ {G : Type u_1} [AddGroup G] {x : G} [Fintype G] : addOrderOf x ∣ Fintype.card G

theorem orderOf_dvd_card_univ {G : Type u_1} [Group G] {x : G} [Fintype G] : orderOf x ∣ Fintype.card G

theorem addOrderOf_dvd_nat_card {G : Type u_6} [AddGroup G] {x : G} : addOrderOf x ∣ Nat.card G

theorem orderOf_dvd_nat_card {G : Type u_6} [Group G] {x : G} : orderOf x ∣ Nat.card G

@[simp]

theorem card_nsmul_eq_zero' {G : Type u_6} [AddGroup G] {x : G} : Nat.card G • x = 0

@[simp]

theorem pow_card_eq_one' {G : Type u_6} [Group G] {x : G} : x ^ Nat.card G = 1

@[simp]

theorem card_nsmul_eq_zero {G : Type u_1} [AddGroup G] {x : G} [Fintype G] : Fintype.card G • x = 0

@[simp]

theorem pow_card_eq_one {G : Type u_1} [Group G] {x : G} [Fintype G] : x ^ Fintype.card G = 1

theorem AddSubgroup.nsmul_index_mem {G : Type u_6} [AddGroup G] (H : AddSubgroup G) [AddSubgroup.Normal H] (g : G) : AddSubgroup.index H • g ∈ H

theorem Subgroup.pow_index_mem {G : Type u_6} [Group G] (H : Subgroup G) [Subgroup.Normal H] (g : G) : g ^ Subgroup.index H ∈ H

theorem nsmul_eq_mod_card {G : Type u_1} [AddGroup G] {x : G} [Fintype G] (n : ℕ) : n • x = (n % Fintype.card G) • x

theorem pow_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} [AddGroup G] {x : G} [Fintype G] (n : ℤ) : n • x = (n % ↑(Fintype.card G)) • x

theorem zpow_eq_mod_card {G : Type u_1} [Group G] {x : G} [Fintype G] (n : ℤ) : x ^ n = x ^ (n % ↑(Fintype.card G))

noncomputable def nsmulCoprime {n : ℕ} {G : Type u_6} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) : G ≃ G

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

Equations

• One or more equations did not get rendered due to their size.

theorem nsmulCoprime.proof_2 {n : ℕ} {G : Type u_1} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) (g : G) : n • Nat.gcdB (Nat.card G) n • g = g

theorem nsmulCoprime.proof_1 {n : ℕ} {G : Type u_1} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) (g : G) : Nat.gcdB (Nat.card G) n • n • g = g

@[simp]

theorem powCoprime_symm_apply {n : ℕ} {G : Type u_6} [Group G] (h : Nat.Coprime (Nat.card G) n) (g : G) : ↑(powCoprime h).symm g = g ^ Nat.gcdB (Nat.card G) n

@[simp]

theorem nsmulCoprime_symm_apply {n : ℕ} {G : Type u_6} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) (g : G) : ↑(nsmulCoprime h).symm g = Nat.gcdB (Nat.card G) n • g

@[simp]

theorem nsmulCoprime_apply {n : ℕ} {G : Type u_6} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) (g : G) : ↑(nsmulCoprime h) g = n • g

@[simp]

theorem powCoprime_apply {n : ℕ} {G : Type u_6} [Group G] (h : Nat.Coprime (Nat.card G) n) (g : G) : ↑(powCoprime h) g = g ^ n

noncomputable def powCoprime {n : ℕ} {G : Type u_6} [Group G] (h : Nat.Coprime (Nat.card G) n) : G ≃ G

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

Equations

• One or more equations did not get rendered due to their size.

theorem nsmulCoprime_zero {n : ℕ} {G : Type u_6} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) : ↑(nsmulCoprime h) 0 = 0

theorem powCoprime_one {n : ℕ} {G : Type u_6} [Group G] (h : Nat.Coprime (Nat.card G) n) : ↑(powCoprime h) 1 = 1

theorem nsmulCoprime_neg {n : ℕ} {G : Type u_6} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) {g : G} : ↑(nsmulCoprime h) (-g) = -↑(nsmulCoprime h) g

theorem powCoprime_inv {n : ℕ} {G : Type u_6} [Group G] (h : Nat.Coprime (Nat.card G) n) {g : G} : ↑(powCoprime h) g⁻¹ = (↑(powCoprime h) g)⁻¹

theorem add_inf_eq_bot_of_coprime {G : Type u_6} [AddGroup G] {H : AddSubgroup G} {K : AddSubgroup G} [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] (h : Nat.Coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })) : H ⊓ K = ⊥

theorem inf_eq_bot_of_coprime {G : Type u_6} [Group G] {H : Subgroup G} {K : Subgroup G} [Fintype { x // x ∈ H }] [Fintype { x // x ∈ K }] (h : Nat.Coprime (Fintype.card { x // x ∈ H }) (Fintype.card { x // x ∈ K })) : H ⊓ K = ⊥

theorem image_range_addOrderOf {G : Type u_1} [AddGroup G] {x : G} [Fintype G] [DecidableEq G] : Finset.image (fun i => i • x) (Finset.range (addOrderOf x)) = Set.toFinset ↑(AddSubgroup.zmultiples x)

theorem image_range_orderOf {G : Type u_1} [Group G] {x : G} [Fintype G] [DecidableEq G] : Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = Set.toFinset ↑(Subgroup.zpowers x)

theorem gcd_nsmul_card_eq_zero_iff {G : Type u_1} [AddGroup G] {x : G} {n : ℕ} [Fintype G] : n • x = 0 ↔ Nat.gcd n (Fintype.card G) • x = 0

abbrev gcd_nsmul_card_eq_zero_iff.match_1 {G : Type u_1} {n : ℕ} [Fintype G] (motive : Nat.gcd n (Fintype.card G) ∣ n → Prop) : (x : Nat.gcd n (Fintype.card G) ∣ n) → ((m : ℕ) → (hm : n = Nat.gcd n (Fintype.card G) * m) → motive (_ : ∃ c, n = Nat.gcd n (Fintype.card G) * c)) → motive x

Equations

• gcd_nsmul_card_eq_zero_iff.match_1 motive x h_1 = Exists.casesOn x fun w h => h_1 w h

theorem pow_gcd_card_eq_one_iff {G : Type u_1} [Group G] {x : G} {n : ℕ} [Fintype G] : x ^ n = 1 ↔ x ^ Nat.gcd n (Fintype.card G) = 1

theorem addSubmonoidOfIdempotent.proof_1 {M : Type u_1} [AddLeftCancelMonoid M] (S : Set M) (hS2 : S + S = S) (a : M) (ha : a ∈ S) (t : ℕ) : (t + 1) • a ∈ S

def addSubmonoidOfIdempotent {M : Type u_6} [AddLeftCancelMonoid M] [Fintype M] (S : Set M) (hS1 : Set.Nonempty S) (hS2 : S + S = S) : AddSubmonoid M

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

Equations

• One or more equations did not get rendered due to their size.

def submonoidOfIdempotent {M : Type u_6} [LeftCancelMonoid M] [Fintype M] (S : Set M) (hS1 : Set.Nonempty S) (hS2 : S * S = S) : Submonoid M

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

Equations

• One or more equations did not get rendered due to their size.

theorem addSubgroupOfIdempotent.proof_2 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (hS1 : Set.Nonempty S) (hS2 : S + S = S) : 0 ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier

theorem addSubgroupOfIdempotent.proof_3 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (hS1 : Set.Nonempty S) (hS2 : S + S = S) {a : G} (ha : a ∈ { toAddSubsemigroup := { carrier := S, add_mem' := (_ : ∀ {a b : G}, a ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier → b ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier → a + b ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier) }, zero_mem' := (_ : 0 ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier) }.toAddSubsemigroup.carrier) : -a ∈ addSubmonoidOfIdempotent S hS1 hS2

def addSubgroupOfIdempotent {G : Type u_6} [AddGroup G] [Fintype G] (S : Set G) (hS1 : Set.Nonempty S) (hS2 : S + S = S) : AddSubgroup G

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

Equations

• One or more equations did not get rendered due to their size.

theorem addSubgroupOfIdempotent.proof_1 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (hS1 : Set.Nonempty S) (hS2 : S + S = S) : ∀ {a b : G}, a ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier → b ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier → a + b ∈ (addSubmonoidOfIdempotent S hS1 hS2).toAddSubsemigroup.carrier

def subgroupOfIdempotent {G : Type u_6} [Group G] [Fintype G] (S : Set G) (hS1 : Set.Nonempty S) (hS2 : S * S = S) : Subgroup G

A nonempty idempotent subset of a finite group is a subgroup

Equations

• One or more equations did not get rendered due to their size.

def smulCardAddSubgroup {G : Type u_6} [AddGroup G] [Fintype G] (S : Set G) (hS : Set.Nonempty S) : AddSubgroup G

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

Equations

• One or more equations did not get rendered due to their size.

theorem smulCardAddSubgroup.proof_1 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (hS : Set.Nonempty S) : 0 ∈ Fintype.card G • S

@[simp]

theorem smulCardAddSubgroup_coe {G : Type u_6} [AddGroup G] [Fintype G] (S : Set G) (hS : Set.Nonempty S) : ↑(smulCardAddSubgroup S hS) = Fintype.card G • S

@[simp]

theorem powCardSubgroup_coe {G : Type u_6} [Group G] [Fintype G] (S : Set G) (hS : Set.Nonempty S) : ↑(powCardSubgroup S hS) = S ^ Fintype.card G

def powCardSubgroup {G : Type u_6} [Group G] [Fintype G] (S : Set G) (hS : Set.Nonempty S) : Subgroup G

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

Equations

• One or more equations did not get rendered due to their size.

theorem orderOf_abs_ne_one {G : Type u_1} [LinearOrderedRing G] {x : G} (h : |x| ≠ 1) : orderOf x = 0

theorem LinearOrderedRing.orderOf_le_two {G : Type u_1} [LinearOrderedRing G] {x : G} : orderOf x ≤ 2

theorem Prod.add_orderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] (x : α × β) : addOrderOf x = Nat.lcm (addOrderOf x.fst) (addOrderOf x.snd)

theorem Prod.orderOf {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] (x : α × β) : orderOf x = Nat.lcm (orderOf x.fst) (orderOf x.snd)

theorem add_orderOf_fst_dvd_add_orderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} : addOrderOf x.fst ∣ addOrderOf x

theorem orderOf_fst_dvd_orderOf {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} : orderOf x.fst ∣ orderOf x

theorem add_orderOf_snd_dvd_add_orderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} : addOrderOf x.snd ∣ addOrderOf x

theorem orderOf_snd_dvd_orderOf {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} : orderOf x.snd ∣ orderOf x

theorem IsOfFinAddOrder.fst {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} (hx : IsOfFinAddOrder x) : IsOfFinAddOrder x.fst

theorem IsOfFinOrder.fst {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.fst

theorem IsOfFinAddOrder.snd {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} (hx : IsOfFinAddOrder x) : IsOfFinAddOrder x.snd

theorem IsOfFinOrder.snd {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.snd

theorem IsOfFinAddOrder.prod_mk {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {a : α} {b : β} : IsOfFinAddOrder a → IsOfFinAddOrder b → IsOfFinAddOrder (a, b)

theorem IsOfFinOrder.prod_mk {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {a : α} {b : β} : IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)