def AlgebraInLean.isFiniteOrder {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) : Prop

Equations

• AlgebraInLean.isFiniteOrder x = ∃ (n : ℕ), n ≠ 0 ∧ AlgebraInLean.mpow x n = AlgebraInLean.𝕖

noncomputable def AlgebraInLean.order {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) : ℕ

Equations

• AlgebraInLean.order x = if h : AlgebraInLean.isFiniteOrder x then Nat.find h else 0

theorem AlgebraInLean.mpow_order_zero {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (n : ℕ) (h₀ : AlgebraInLean.order x = 0) : AlgebraInLean.mpow x n = AlgebraInLean.𝕖 → n = 0

If xⁿ = e → n = 0

theorem AlgebraInLean.mpow_order {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) : AlgebraInLean.mpow x (AlgebraInLean.order x) = AlgebraInLean.𝕖

If n is the order of x, then xⁿ = e

theorem AlgebraInLean.mpow_mod_order {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) : AlgebraInLean.mpow x (m % AlgebraInLean.order x) = AlgebraInLean.mpow x m

Let m be the order x. Write m = nq + r with 0 ≤ r < m. Then, xʳ = xⁿ

theorem AlgebraInLean.order_divides_iff_mpow_id {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) : AlgebraInLean.mpow x m = AlgebraInLean.𝕖 ↔ AlgebraInLean.order x ∣ m

Let n be the order of x. xᵐ = e ↔ n | m

theorem AlgebraInLean.order_nonzero_iff {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) : AlgebraInLean.order x ≠ 0 ↔ ∃ (n : ℕ), n ≠ 0 ∧ AlgebraInLean.mpow x n = AlgebraInLean.𝕖

The order of x is nonzero if and only if there exists an n : ℕ such that xⁿ = e

theorem AlgebraInLean.order_id {M : Type u_1} [AlgebraInLean.Monoid M] : AlgebraInLean.order AlgebraInLean.𝕖 = 1

The order of the identity element, 𝕖, in any monoid is 1.

theorem AlgebraInLean.mpow_nonzero_order {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (n : ℕ) (h : AlgebraInLean.order x ≠ 0) : AlgebraInLean.order (AlgebraInLean.mpow x n) ≠ 0

Let m be the order of x and let n : ℕ with n ≠ 0. If m ≠ 0, then the order of xⁿ is nonzero

theorem AlgebraInLean.inverse_of_nonzero_order {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (h : AlgebraInLean.order x ≠ 0) : ∃ (y : M), AlgebraInLean.μ x y = AlgebraInLean.𝕖 ∧ AlgebraInLean.μ y x = AlgebraInLean.𝕖

theorem AlgebraInLean.mpow_inj_of_lt_order {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) (n : ℕ) (hm : m < AlgebraInLean.order x) (hn : n < AlgebraInLean.order x) : AlgebraInLean.mpow x m = AlgebraInLean.mpow x n → m = n

Suppose m, n < order x. If xᵐ = xⁿ, then m = n

theorem AlgebraInLean.mod_order_eq_of_mpow_eq {M : Type u_1} [AlgebraInLean.Monoid M] (x : M) (m : ℕ) (n : ℕ) (h : AlgebraInLean.order x ≠ 0) : AlgebraInLean.mpow x m = AlgebraInLean.mpow x n → m % AlgebraInLean.order x = n % AlgebraInLean.order x

Let r ≠ 0 be the order of x. If xᵐ = xⁿ, then m is congruent to n (mod r)

theorem AlgebraInLean.gpow_order {G : Type u_1} [AlgebraInLean.Group G] (x : G) : AlgebraInLean.gpow x ↑(AlgebraInLean.order x) = AlgebraInLean.𝕖

Let n be the order x. Then, xⁿ = 𝕖

theorem AlgebraInLean.gpow_id {G : Type u_1} [AlgebraInLean.Group G] (n : ℤ) : AlgebraInLean.gpow AlgebraInLean.𝕖 n = AlgebraInLean.𝕖

theorem AlgebraInLean.gpow_order_zero {G : Type u_1} [AlgebraInLean.Group G] (x : G) {n : ℤ} (h₀ : AlgebraInLean.order x = 0) : AlgebraInLean.gpow x n = AlgebraInLean.𝕖 → n = 0

Suppose the order of x is 0. Then if xⁿ = 𝕖, n = 0

theorem AlgebraInLean.gpow_mod_order {G : Type u_1} [AlgebraInLean.Group G] (x : G) {n : ℤ} : AlgebraInLean.gpow x (n % ↑(AlgebraInLean.order x)) = AlgebraInLean.gpow x n

Let m be the order x. Write m = nq + r with 0 ≤ r < m. Then, xʳ = xⁿ

theorem AlgebraInLean.gpow_inj_of_order_zero {G : Type u_1} [AlgebraInLean.Group G] (x : G) {m : ℤ} {n : ℤ} (h : AlgebraInLean.order x = 0) (heq : AlgebraInLean.gpow x m = AlgebraInLean.gpow x n) : m = n

Suppose the order of x is 0. Then xᵐ = xⁿ → m = n

theorem AlgebraInLean.emod_has_nat {m : ℕ} (n : ℤ) (hm : 0 < m) : ∃ (n' : ℕ), n % ↑m = ↑n' % ↑m

theorem AlgebraInLean.mod_order_eq_of_gpow_eq {G : Type u_1} [AlgebraInLean.Group G] (x : G) {m : ℤ} {n : ℤ} : AlgebraInLean.gpow x m = AlgebraInLean.gpow x n → m % ↑(AlgebraInLean.order x) = n % ↑(AlgebraInLean.order x)

The capstone theorem of gpow: let r = order x. Then if two integers m and n satisfy xᵐ = xⁿ, then m ≡ n [MOD order x]. If r = 0, then m = n.