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_mul_iff_pow_eq_one {G : Type u_1} [Monoid G] {n : ℕ} (x : G) : Function.IsPeriodicPt (fun (x_1 : G) => x * x_1) n 1 ↔ x ^ n = 1

theorem isPeriodicPt_add_iff_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {n : ℕ} (x : G) : Function.IsPeriodicPt (fun (x_1 : G) => x + x_1) n 0 ↔ n • x = 0

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_1 : G) => x * x_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_1 : G) => x + x_1)

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

theorem isOfFinOrder_ofAdd_iff {α : Type u_6} [AddMonoid α] {x : α} : IsOfFinOrder (Multiplicative.ofAdd x) ↔ IsOfFinAddOrder x

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

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

theorem IsOfFinOrder.exists_pow_eq_one {G : Type u_1} [Monoid G] {x : G} : IsOfFinOrder x → ∃ (n : ℕ), 0 < n ∧ x ^ n = 1

Alias of the forward direction of isOfFinOrder_iff_pow_eq_one.

theorem IsOfFinAddOrder.exists_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} : IsOfFinAddOrder x → ∃ (n : ℕ), 0 < n ∧ n • x = 0

Alias of the forward direction of isOfFinAddOrder_iff_nsmul_eq_zero.

theorem isOfFinOrder_iff_zpow_eq_one {G : Type u_6} [DivisionMonoid G] {x : G} : IsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1

theorem isOfFinAddOrder_iff_zsmul_eq_zero {G : Type u_6} [SubtractionMonoid G] {x : G} : IsOfFinAddOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ n • x = 0

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

@[simp]

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

1 is of finite order in any monoid.

@[simp]

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

0 is of finite order in any additive monoid.

theorem IsOfFinOrder.pow {G : Type u_1} [Monoid G] {a : G} {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n)

theorem IsOfFinAddOrder.nsmul {G : Type u_1} [AddMonoid G] {a : G} {n : ℕ} : IsOfFinAddOrder a → IsOfFinAddOrder (n • a)

theorem IsOfFinOrder.of_pow {G : Type u_1} [Monoid G] {a : G} {n : ℕ} (h : IsOfFinOrder (a ^ n)) (hn : n ≠ 0) : IsOfFinOrder a

theorem IsOfFinAddOrder.of_nsmul {G : Type u_1} [AddMonoid G] {a : G} {n : ℕ} (h : IsOfFinAddOrder (n • a)) (hn : n ≠ 0) : IsOfFinAddOrder a

@[simp]

theorem isOfFinOrder_pow {G : Type u_1} [Monoid G] {a : G} {n : ℕ} : IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

@[simp]

theorem isOfFinAddOrder_nsmul {G : Type u_1} [AddMonoid G] {a : G} {n : ℕ} : IsOfFinAddOrder (n • a) ↔ IsOfFinAddOrder a ∨ n = 0

theorem not_isOfFinOrder_of_isMulTorsionFree {G : Type u_1} [Monoid G] {a : G} [IsMulTorsionFree G] (ha : a ≠ 1) : ¬IsOfFinOrder a

theorem not_isOfFinAddOrder_of_isAddTorsionFree {G : Type u_1} [AddMonoid G] {a : G} [IsAddTorsionFree G] (ha : a ≠ 0) : ¬IsOfFinAddOrder a

theorem IsOfFinOrder.eq_one' {G : Type u_1} [Monoid G] [IsMulTorsionFree G] {a : G} (ha : IsOfFinOrder a) : a = 1

theorem IsOfFinAddOrder.eq_zero' {G : Type u_1} [AddMonoid G] [IsAddTorsionFree G] {a : G} (ha : IsOfFinAddOrder a) : a = 0

theorem isOfFinOrder_iff_eq_one {G : Type u_1} [Monoid G] [IsMulTorsionFree G] (a : G) : IsOfFinOrder a ↔ a = 1

theorem isOfFinAddOrder_iff_eq_zero {G : Type u_1} [AddMonoid G] [IsAddTorsionFree G] (a : G) : IsOfFinAddOrder a ↔ a = 0

theorem Submonoid.isOfFinOrder_coe {G : Type u_1} [Monoid G] {H : Submonoid G} {x : ↥H} : IsOfFinOrder ↑x ↔ IsOfFinOrder x

Elements of finite order are of finite order in submonoids.

theorem AddSubmonoid.isOfFinAddOrder_coe {G : Type u_1} [AddMonoid G] {H : AddSubmonoid G} {x : ↥H} : IsOfFinAddOrder ↑x ↔ IsOfFinAddOrder x

Elements of finite order are of finite order in submonoids.

theorem IsConj.isOfFinOrder {G : Type u_1} [Monoid G] {x y : G} (h : IsConj x y) : IsOfFinOrder x → IsOfFinOrder y

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

@[reducible, inline]

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

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

Equations

• hx.groupPowers = And.casesOn ⋯ fun (hpos : 0 < ⋯.choose) (hx_1 : x ^ ⋯.choose = 1) => Submonoid.groupPowers hpos hx_1

@[reducible, inline]

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

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

Equations

• hx.addGroupMultiples = And.casesOn ⋯ fun (hpos : 0 < ⋯.choose) (hx_1 : ⋯.choose • x = 0) => AddSubmonoid.addGroupMultiples hpos hx_1

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_1 : G) => x * x_1) 1

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_1 : G) => x + x_1) 0

theorem Subsingleton.orderOf_eq {G : Type u_1} [Monoid G] [Subsingleton G] (x : G) : orderOf x = 1

theorem Subsingleton.addOrderOf_eq {G : Type u_1} [AddMonoid G] [Subsingleton G] (x : G) : addOrderOf 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 {α : Type u_6} [AddMonoid α] (a : α) : orderOf (Multiplicative.ofAdd a) = addOrderOf a

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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 ↔ ∀ (n : ℕ), 0 < n → x ^ n ≠ 1

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

theorem orderOf_ne_zero_iff {G : Type u_1} [Monoid G] {x : G} : orderOf x ≠ 0 ↔ IsOfFinOrder x

theorem addOrderOf_ne_zero_iff {G : Type u_1} [AddMonoid G] {x : G} : addOrderOf x ≠ 0 ↔ IsOfFinAddOrder x

@[simp]

theorem orderOf_zero (M₀ : Type u_6) [MonoidWithZero M₀] [Nontrivial M₀] : orderOf 0 = 0

In a nontrivial monoid with zero, the order of the zero element is zero.

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

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

@[simp]

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.

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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_of_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (h : n • x = 0) : addOrderOf x ∣ n

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

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

theorem exists_pow_eq_pow_two_mul {G : Type u_1} [Monoid G] {x : G} {p : ℕ} (hx : x ^ p = 1) (hp : Odd p) (n : ℕ) : ∃ (m : ℕ), x ^ n = x ^ (2 * m)

If x ^ p = 1 for some odd p, then every power of x is an even power of x.

theorem exists_nsmul_eq_nsmul_two_add {G : Type u_1} [AddMonoid G] {x : G} {p : ℕ} (hx : p • x = 0) (hp : Odd p) (n : ℕ) : ∃ (m : ℕ), n • x = (2 * m) • x

If p • x = 0 for some odd p, then every multiple of x is an even multiple of x.

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

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

theorem pow_injOn_Iio_orderOf {G : Type u_1} [Monoid G] {x : G} : Set.InjOn (fun (x_1 : ℕ) => x ^ x_1) (Set.Iio (orderOf x))

theorem nsmul_injOn_Iio_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} : Set.InjOn (fun (x_1 : ℕ) => x_1 • x) (Set.Iio (addOrderOf x))

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

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

theorem IsOfFinOrder.powers_eq_image_range_orderOf {G : Type u_1} [Monoid G] {x : G} [DecidableEq G] (hx : IsOfFinOrder x) : ↑(Submonoid.powers x) = ↑(Finset.image (fun (x_1 : ℕ) => x ^ x_1) (Finset.range (orderOf x)))

theorem IsOfFinAddOrder.multiples_eq_image_range_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} [DecidableEq G] (hx : IsOfFinAddOrder x) : ↑(AddSubmonoid.multiples x) = ↑(Finset.image (fun (x_1 : ℕ) => x_1 • x) (Finset.range (addOrderOf x)))

theorem pow_eq_pow_of_modEq {G : Type u_1} [Monoid G] {x : G} {n a b : ℕ} (h : a ≡ b [MOD n]) (hx : x ^ n = 1) : x ^ a = x ^ b

theorem nsmul_eq_nsmul_of_modEq {G : Type u_1} [AddMonoid G] {x : G} {n a b : ℕ} (h : a ≡ b [MOD n]) (hx : n • x = 0) : a • x = b • 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 nsmul_eq_zero_iff_modEq {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} : n • x = 0 ↔ n ≡ 0 [MOD 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 addOrderOf_map_dvd {G : Type u_1} [AddMonoid G] {H : Type u_6} [AddMonoid H] (ψ : G →+ H) (x : G) : addOrderOf (ψ x) ∣ addOrderOf x

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

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

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

An injective homomorphism of monoids preserves orders of elements.

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

An injective homomorphism of additive monoids preserves orders of elements.

@[simp]

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

A multiplicative equivalence preserves orders of elements.

@[simp]

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

An additive equivalence preserves orders of elements.

theorem Function.Injective.isOfFinOrder_iff {G : Type u_1} {H : Type u_2} [Monoid G] {x : G} [Monoid H] {f : G →* H} (hf : Injective ⇑f) : IsOfFinOrder (f x) ↔ IsOfFinOrder x

theorem Function.Injective.isOfFinAddOrder_iff {G : Type u_1} {H : Type u_2} [AddMonoid G] {x : G} [AddMonoid H] {f : G →+ H} (hf : Injective ⇑f) : IsOfFinAddOrder (f x) ↔ IsOfFinAddOrder x

@[simp]

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

@[simp]

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

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

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

theorem IsUnit.orderOf_eq_one {G : Type u_1} [Monoid G] [Subsingleton Gˣ] {x : G} (h : IsUnit x) : orderOf x = 1

theorem IsAddUnit.addOrderOf_eq_zero {G : Type u_1} [AddMonoid G] [Subsingleton (AddUnits G)] {x : G} (h : IsAddUnit x) : addOrderOf x = 1

theorem Units.isOfFinOrder_val {G : Type u_1} [Monoid G] {u : Gˣ} : IsOfFinOrder ↑u ↔ IsOfFinOrder u

theorem AddUnits.isOfFinAddOrder_val {G : Type u_1} [AddMonoid G] {u : AddUnits G} : IsOfFinAddOrder ↑u ↔ IsOfFinAddOrder u

noncomputable def IsOfFinOrder.unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) : Mˣ

If the order of x is finite, then x is a unit with inverse x ^ (orderOf x - 1).

Equations

• hx.unit = { val := x, inv := x ^ (orderOf x - 1), val_inv := ⋯, inv_val := ⋯ }

noncomputable def IsOfFinAddOrder.addUnit {M : Type u_6} [AddMonoid M] {x : M} (hx : IsOfFinAddOrder x) : AddUnits M

If the additive order of x is finite, then x is an additive unit with inverse (addOrderOf x - 1) • x.

Equations

• hx.addUnit = { val := x, neg := (addOrderOf x - 1) • x, val_neg := ⋯, neg_val := ⋯ }

@[simp]

theorem IsOfFinAddOrder.val_addUnit {M : Type u_6} [AddMonoid M] {x : M} (hx : IsOfFinAddOrder x) : ↑hx.addUnit = x

@[simp]

theorem IsOfFinAddOrder.val_neg_addUnit {M : Type u_6} [AddMonoid M] {x : M} (hx : IsOfFinAddOrder x) : ↑(-hx.addUnit) = (addOrderOf x - 1) • x

@[simp]

theorem IsOfFinOrder.val_inv_unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) : ↑hx.unit⁻¹ = x ^ (orderOf x - 1)

@[simp]

theorem IsOfFinOrder.val_unit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) : ↑hx.unit = x

theorem IsOfFinOrder.isUnit {M : Type u_6} [Monoid M] {x : M} (hx : IsOfFinOrder x) : IsUnit x

theorem IsOfFinAddOrder.isAddUnit {M : Type u_6} [AddMonoid M] {x : M} (hx : IsOfFinAddOrder x) : IsAddUnit x

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

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

theorem orderOf_pow_of_dvd {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ orderOf x) : orderOf (x ^ n) = orderOf x / n

theorem addOrderOf_nsmul_of_dvd {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ addOrderOf x) : addOrderOf (n • x) = addOrderOf x / n

theorem orderOf_pow_orderOf_div {G : Type u_1} [Monoid G] {x : G} {n : ℕ} (hx : orderOf x ≠ 0) (hn : n ∣ orderOf x) : orderOf (x ^ (orderOf x / n)) = n

theorem addOrderOf_nsmul_addOrderOf_sub {G : Type u_1} [AddMonoid G] {x : G} {n : ℕ} (hx : addOrderOf x ≠ 0) (hn : n ∣ addOrderOf x) : addOrderOf ((addOrderOf x / n) • x) = n

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

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

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

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

theorem IsOfFinOrder.natCard_powers_le_orderOf {G : Type u_1} [Monoid G] {a : G} (ha : IsOfFinOrder a) : Nat.card ↑↑(Submonoid.powers a) ≤ orderOf a

theorem IsOfFinAddOrder.natCard_multiples_le_addOrderOf {G : Type u_1} [AddMonoid G] {a : G} (ha : IsOfFinAddOrder a) : Nat.card ↑↑(AddSubmonoid.multiples a) ≤ addOrderOf a

theorem IsOfFinOrder.finite_powers {G : Type u_1} [Monoid G] {a : G} (ha : IsOfFinOrder a) : (↑(Submonoid.powers a)).Finite

theorem IsOfFinAddOrder.finite_multiples {G : Type u_1} [AddMonoid G] {a : G} (ha : IsOfFinAddOrder a) : (↑(AddSubmonoid.multiples a)).Finite

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

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

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

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

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

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

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

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

theorem Commute.isOfFinOrder_mul {G : Type u_1} [Monoid G] {x 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.isOfFinAddOrder_add {G : Type u_1} [AddMonoid G] {x 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.orderOf_mul_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [Monoid G] {x 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 AddCommute.addOrderOf_add_eq_right_of_forall_prime_mul_dvd {G : Type u_1} [AddMonoid G] {x 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_left_of_forall_prime_mul_dvd {G : Type u_1} [Monoid G] {x y : G} (h : Commute x y) (hx : IsOfFinOrder x) (hdvd : ∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x) : orderOf (x * y) = orderOf x

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

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

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

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

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

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

The backward direction of orderOf_eq_prime_iff.

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

The backward direction of addOrderOf_eq_prime_iff.

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)

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

@[simp]

theorem orderOf_neg_one {R : Type u_6} [Ring R] [Nontrivial R] : orderOf (-1) = if ringChar R = 2 then 1 else 2

theorem CharP.orderOf_eq_two_iff {R : Type u_6} [Ring R] [Nontrivial R] [NoZeroDivisors R] (p : ℕ) (hp : p ≠ 2) [CharP R p] {x : R} : orderOf x = 2 ↔ x = -1

noncomputable def finEquivPowers {G : Type u_1} [Monoid G] {x : G} (hx : IsOfFinOrder x) : Fin (orderOf x) ≃ ↥(Submonoid.powers x)

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

Equations

• finEquivPowers hx = Equiv.ofBijective (fun (n : Fin (orderOf x)) => ⟨x ^ ↑n, ⋯⟩) ⋯

noncomputable def finEquivMultiples {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) : Fin (addOrderOf x) ≃ ↥(AddSubmonoid.multiples x)

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

Equations

• finEquivMultiples hx = Equiv.ofBijective (fun (n : Fin (addOrderOf x)) => ⟨↑n • x, ⋯⟩) ⋯

@[simp]

theorem finEquivPowers_apply {G : Type u_1} [Monoid G] {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)} : (finEquivPowers hx) n = ⟨x ^ ↑n, ⋯⟩

@[simp]

theorem finEquivMultiples_apply {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) {n : Fin (addOrderOf x)} : (finEquivMultiples hx) n = ⟨↑n • x, ⋯⟩

@[simp]

theorem finEquivPowers_symm_apply {G : Type u_1} [Monoid G] {x : G} (hx : IsOfFinOrder x) (n : ℕ) : (finEquivPowers hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩

@[simp]

theorem finEquivMultiples_symm_apply {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) (n : ℕ) : (finEquivMultiples hx).symm ⟨n • x, ⋯⟩ = ⟨n % addOrderOf x, ⋯⟩

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

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

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

theorem IsOfFinAddOrder.nsmul_inj_mod {G : Type u_1} [AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) {n m : ℕ} : n • x = m • x ↔ n % addOrderOf x = m % 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]

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]

@[simp]

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

@[simp]

theorem injective_nsmul_iff_not_isOfFinAddOrder {G : Type u_1} [AddLeftCancelMonoid G] {x : G} : (Function.Injective fun (n : ℕ) => n • x) ↔ ¬IsOfFinAddOrder 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_mod {G : Type u_1} [AddLeftCancelMonoid G] {x : G} {n m : ℕ} : n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x

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 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 infinite_not_isOfFinOrder {G : Type u_1} [LeftCancelMonoid G] {x : G} (h : ¬IsOfFinOrder x) : {y : G | ¬IsOfFinOrder y}.Infinite

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

@[simp]

theorem finite_powers {G : Type u_1} [LeftCancelMonoid G] {a : G} : (↑(Submonoid.powers a)).Finite ↔ IsOfFinOrder a

@[simp]

theorem finite_multiples {G : Type u_1} [AddLeftCancelMonoid G] {a : G} : (↑(AddSubmonoid.multiples a)).Finite ↔ IsOfFinAddOrder a

@[simp]

theorem infinite_powers {G : Type u_1} [LeftCancelMonoid G] {a : G} : (↑(Submonoid.powers a)).Infinite ↔ ¬IsOfFinOrder a

@[simp]

theorem infinite_multiples {G : Type u_1} [AddLeftCancelMonoid G] {a : G} : (↑(AddSubmonoid.multiples a)).Infinite ↔ ¬IsOfFinAddOrder a

theorem Nat.card_submonoidPowers {G : Type u_1} [LeftCancelMonoid G] {a : G} : Nat.card ↥(Submonoid.powers a) = orderOf a

See also orderOf_eq_card_powers.

theorem Nat.card_addSubmonoidMultiples {G : Type u_1} [AddLeftCancelMonoid G] {a : G} : Nat.card ↥(AddSubmonoid.multiples a) = addOrderOf a

See also addOrder_eq_card_multiples.

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

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

@[simp]

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

@[simp]

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

theorem RightCancelMonoid.pow_inj_mod {G : Type u_1} [RightCancelMonoid G] {x : G} {n m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x

theorem AddRightCancelMonoid.nsmul_inj_mod {G : Type u_1} [AddRightCancelMonoid G] {x : G} {n m : ℕ} : n • x = m • x ↔ n % addOrderOf x = m % addOrderOf x

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

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

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

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

@[simp]

theorem RightCancelMonoid.finite_powers {G : Type u_1} [RightCancelMonoid G] {a : G} : (↑(Submonoid.powers a)).Finite ↔ IsOfFinOrder a

@[simp]

theorem AddRightCancelMonoid.finite_multiples {G : Type u_1} [AddRightCancelMonoid G] {a : G} : (↑(AddSubmonoid.multiples a)).Finite ↔ IsOfFinAddOrder a

@[simp]

theorem RightCancelMonoid.infinite_powers {G : Type u_1} [RightCancelMonoid G] {a : G} : (↑(Submonoid.powers a)).Infinite ↔ ¬IsOfFinOrder a

@[simp]

theorem AddRightCancelMonoid.infinite_multiples {G : Type u_1} [AddRightCancelMonoid G] {a : G} : (↑(AddSubmonoid.multiples a)).Infinite ↔ ¬IsOfFinAddOrder a

theorem RightCancelMonoid.Nat.card_submonoidPowers {G : Type u_1} [RightCancelMonoid G] {a : G} : Nat.card ↥(Submonoid.powers a) = orderOf a

See also orderOf_eq_card_powers.

theorem AddRightCancelMonoid.Nat.card_addSubmonoidMultiples {G : Type u_1} [AddRightCancelMonoid G] {a : G} : Nat.card ↥(AddSubmonoid.multiples a) = addOrderOf a

See also addOrder_eq_card_multiples.

@[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.

@[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.

theorem IsOfFinOrder.of_inv {G : Type u_1} [Group G] {x : G} : IsOfFinOrder x⁻¹ → IsOfFinOrder x

Alias of the forward direction of isOfFinOrder_inv_iff.

---

Inverses of elements of finite order have finite order.

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

Alias of the reverse direction of isOfFinOrder_inv_iff.

---

Inverses of elements of finite order have finite order.

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

Alias of the forward direction of isOfFinAddOrder_neg_iff.

---

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

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

Alias of the reverse direction of isOfFinAddOrder_neg_iff.

---

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

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

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

@[simp]

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

@[simp]

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

theorem orderOf_dvd_sub_iff_zpow_eq_zpow {G : Type u_1} [Group G] {x : G} {a b : ℤ} : ↑(orderOf x) ∣ a - b ↔ x ^ a = x ^ b

theorem addOrderOf_dvd_sub_iff_zsmul_eq_zsmul {G : Type u_1} [AddGroup G] {x : G} {a b : ℤ} : ↑(addOrderOf x) ∣ a - b ↔ a • x = b • x

theorem Subgroup.orderOf_coe {G : Type u_1} [Group G] {H : Subgroup G} (a : ↥H) : orderOf ↑a = orderOf a

theorem AddSubgroup.addOrderOf_coe {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (a : ↥H) : addOrderOf ↑a = addOrderOf a

@[simp]

theorem Subgroup.orderOf_mk {G : Type u_1} [Group G] {H : Subgroup G} (a : G) (ha : a ∈ H) : orderOf ⟨a, ha⟩ = orderOf a

@[simp]

theorem AddSubgroup.addOrderOf_mk {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (a : G) (ha : a ∈ H) : addOrderOf ⟨a, ha⟩ = addOrderOf a

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

theorem smul_eq_self_of_mem_zpowers {G : Type u_1} [Group G] {x 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 {G : Type u_6} [AddGroup G] {x y : G} {α : Type u_7} [AddAction G α] (hx : x ∈ AddSubgroup.zmultiples y) {a : α} (hs : y +ᵥ a = a) : x +ᵥ a = a

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

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

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

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

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

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

theorem Subgroup.closure_toSubmonoid_of_isOfFinOrder {G : Type u_1} [Group G] {s : Set G} (hs : ∀ x ∈ s, IsOfFinOrder x) : (closure s).toSubmonoid = Submonoid.closure s

See Subgroup.closure_toSubmonoid_of_finite for a version for finite groups.

theorem AddSubgroup.closure_toAddSubmonoid_of_isOfFinAddOrder {G : Type u_1} [AddGroup G] {s : Set G} (hs : ∀ x ∈ s, IsOfFinAddOrder x) : (closure s).toAddSubmonoid = AddSubmonoid.closure s

See AddSubgroup.closure_toAddSubmonoid_of_finite for a version for finite additive groups.

noncomputable def finEquivZPowers {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) : Fin (orderOf x) ≃ ↥(Subgroup.zpowers x)

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

Equations

• finEquivZPowers hx = (finEquivPowers hx).trans (Equiv.setCongr ⋯)

noncomputable def finEquivZMultiples {G : Type u_1} [AddGroup G] {x : G} (hx : IsOfFinAddOrder x) : Fin (addOrderOf x) ≃ ↥(AddSubgroup.zmultiples x)

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

Equations

• finEquivZMultiples hx = (finEquivMultiples hx).trans (Equiv.setCongr ⋯)

theorem finEquivZPowers_apply {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)} : (finEquivZPowers hx) n = ⟨x ^ ↑n, ⋯⟩

theorem finEquivZMultiples_apply {G : Type u_1} [AddGroup G] {x : G} (hx : IsOfFinAddOrder x) {n : Fin (addOrderOf x)} : (finEquivZMultiples hx) n = ⟨↑n • x, ⋯⟩

theorem finEquivZPowers_symm_apply {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) (n : ℕ) : (finEquivZPowers hx).symm ⟨x ^ n, ⋯⟩ = ⟨n % orderOf x, ⋯⟩

theorem finEquivZMultiples_symm_apply {G : Type u_1} [AddGroup G] {x : G} (hx : IsOfFinAddOrder x) (n : ℕ) : (finEquivZMultiples hx).symm ⟨n • x, ⋯⟩ = ⟨n % addOrderOf x, ⋯⟩

theorem pow_finEquivZPowers_symm_apply {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) (a : ↥(Subgroup.zpowers x)) : x ^ ↑((finEquivZPowers hx).symm a) = ↑a

theorem nsmul_finEquivZMultiples_symm_apply {G : Type u_1} [AddGroup G] {x : G} (hx : IsOfFinAddOrder x) (a : ↥(AddSubgroup.zmultiples x)) : ↑((finEquivZMultiples hx).symm a) • x = ↑a

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

Elements of finite order are closed under multiplication.

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

Elements of finite additive order are closed under addition.

theorem isMulTorsionFree_iff_not_isOfFinOrder {G : Type u_1} [CommGroup G] : IsMulTorsionFree G ↔ ∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a

theorem isAddTorsionFree_iff_not_isOfFinAddOrder {G : Type u_1} [AddCommGroup G] : IsAddTorsionFree G ↔ ∀ ⦃a : G⦄, a ≠ 0 → ¬IsOfFinAddOrder a

theorem IsMulTorsionFree.of_not_isOfFinOrder {G : Type u_1} [CommGroup G] : (∀ ⦃a : G⦄, a ≠ 1 → ¬IsOfFinOrder a) → IsMulTorsionFree G

Alias of the reverse direction of isMulTorsionFree_iff_not_isOfFinOrder.

theorem IsAddTorsionFree.of_not_isOfFinAddOrder {G : Type u_1} [AddCommGroup G] : (∀ ⦃a : G⦄, a ≠ 0 → ¬IsOfFinAddOrder a) → IsAddTorsionFree G

Alias of the reverse direction of isAddTorsionFree_iff_not_isOfFinAddOrder.

theorem not_isMulTorsionFree_iff_isOfFinOrder {G : Type u_1} [CommGroup G] : ¬IsMulTorsionFree G ↔ ∃ (a : G), a ≠ 1 ∧ IsOfFinOrder a

theorem not_isAddTorsionFree_iff_isOfFinAddOrder {G : Type u_1} [AddCommGroup G] : ¬IsAddTorsionFree G ↔ ∃ (a : G), a ≠ 0 ∧ IsOfFinAddOrder a

@[simp]

theorem zpowers_mabs {G : Type u_1} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] (g : G) : Subgroup.zpowers |g|ₘ = Subgroup.zpowers g

@[simp]

theorem zmultiples_abs {G : Type u_1} [AddCommGroup G] [LinearOrder G] [IsOrderedAddMonoid G] (g : G) : AddSubgroup.zmultiples |g| = AddSubgroup.zmultiples g

theorem IsMulTorsionFree.orderOf_le_one {G : Type u_1} [CommGroup G] [IsMulTorsionFree G] (g : G) : orderOf g ≤ 1

theorem IsAddTorsionFree.addOrderOf_nonpos {G : Type u_1} [AddCommGroup G] [IsAddTorsionFree G] (g : G) : addOrderOf g ≤ 1

theorem sum_card_orderOf_eq_card_pow_eq_one {G : Type u_1} [Monoid G] {n : ℕ} [Fintype G] [DecidableEq G] (hn : n ≠ 0) : ∑ m ∈ n.divisors, {x : G | orderOf x = m}.card = {x : G | x ^ n = 1}.card

theorem sum_card_addOrderOf_eq_card_nsmul_eq_zero {G : Type u_1} [AddMonoid G] {n : ℕ} [Fintype G] [DecidableEq G] (hn : n ≠ 0) : ∑ m ∈ n.divisors, {x : G | addOrderOf x = m}.card = {x : G | n • x = 0}.card

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

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

theorem orderOf_le_card {G : Type u_1} [Monoid G] {x : G} [Finite G] : orderOf x ≤ Nat.card G

theorem addOrderOf_le_card {G : Type u_1} [AddMonoid G] {x : G} [Finite G] : addOrderOf x ≤ Nat.card G

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

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

@[instance_reducible]

noncomputable def LeftCancelMonoid.groupOfFinite {G : Type u_1} [LeftCancelMonoid G] [Finite G] : Group G

Every finite left cancellative monoid is a group.

Equations

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

@[instance_reducible]

noncomputable def AddLeftCancelMonoid.addGroupOfFinite {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] : AddGroup G

Every finite left cancellative additive monoid is an additive group.

Equations

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

@[instance_reducible]

noncomputable def RightCancelMonoid.groupOfFinite {H : Type u_6} [RightCancelMonoid H] [Finite H] : Group H

Every finite right cancellative monoid is a group.

Equations

• RightCancelMonoid.groupOfFinite = (MulEquiv.opOp H).group

@[instance_reducible]

noncomputable def AddRightCancelMonoid.addGroupOfFinite {H : Type u_6} [AddRightCancelMonoid H] [Finite H] : AddGroup H

Every finite right cancellative additive monoid is an additive group.

Equations

• AddRightCancelMonoid.addGroupOfFinite = (AddEquiv.opOp H).addGroup

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

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

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

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

theorem orderOf_pow {G : Type u_1} [LeftCancelMonoid G] [Finite G] {n : ℕ} (x : G) : orderOf (x ^ n) = orderOf x / (orderOf x).gcd n

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

theorem addOrderOf_nsmul {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {n : ℕ} (x : G) : addOrderOf (n • x) = addOrderOf x / (addOrderOf x).gcd n

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

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

theorem mem_multiples_iff_mem_range_addOrderOf {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {x y : G} [DecidableEq G] : y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun (x_1 : ℕ) => x_1 • x) (Finset.range (addOrderOf x))

noncomputable def powersEquivPowers {G : Type u_1} [LeftCancelMonoid G] [Finite G] {x y : 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 ⋯).symm.trans ((finCongr h).trans (finEquivPowers ⋯))

noncomputable def multiplesEquivMultiples {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {x y : 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 ⋯).symm.trans ((finCongr h).trans (finEquivMultiples ⋯))

@[simp]

theorem powersEquivPowers_apply {G : Type u_1} [LeftCancelMonoid G] [Finite G] {x y : G} (h : orderOf x = orderOf y) (n : ℕ) : (powersEquivPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

@[simp]

theorem multiplesEquivMultiples_apply {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] {x y : G} (h : addOrderOf x = addOrderOf y) (n : ℕ) : (multiplesEquivMultiples h) ⟨n • x, ⋯⟩ = ⟨n • y, ⋯⟩

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

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

theorem isOfFinOrder_iff_isUnit {G : Type u_1} [Monoid G] [Finite Gˣ] {x : G} : IsOfFinOrder x ↔ IsUnit x

theorem IsUnit.isOfFinOrder {G : Type u_1} [Monoid G] [Finite Gˣ] {x : G} : IsUnit x → IsOfFinOrder x

Alias of the reverse direction of isOfFinOrder_iff_isUnit.

theorem orderOf_eq_zero_iff_eq_zero {G₀ : Type u_6} [GroupWithZero G₀] [Finite G₀] {a : G₀} : orderOf a = 0 ↔ a = 0

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_zero_iff_modEq {G : Type u_1} [AddGroup G] {x : G} {n : ℤ} : n • x = 0 ↔ n ≡ 0 [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)]

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)]

@[simp]

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

@[simp]

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

theorem Subgroup.zpowers_eq_zpowers_iff {G : Type u_1} [Group G] {x y : G} (hx : ¬IsOfFinOrder x) : zpowers x = zpowers y ↔ x = y ∨ x⁻¹ = y

theorem AddSubgroup.zmultiples_eq_zmultiples_iff {G : Type u_1} [AddGroup G] {x y : G} (hx : ¬IsOfFinAddOrder x) : zmultiples x = zmultiples y ↔ x = y ∨ -x = y

theorem mem_zpowers_zpow_iff {G : Type u_1} [Group G] {g : G} {k : ℤ} : g ∈ Subgroup.zpowers (g ^ k) ↔ k.gcd ↑(orderOf g) = 1

theorem mem_zmultiples_zsmul_iff {G : Type u_1} [AddGroup G] {g : G} {k : ℤ} : g ∈ AddSubgroup.zmultiples (k • g) ↔ k.gcd ↑(addOrderOf g) = 1

theorem mem_zpowers_pow_iff {G : Type u_1} [Group G] {g : G} {k : ℕ} : g ∈ Subgroup.zpowers (g ^ k) ↔ k.gcd (orderOf g) = 1

theorem mem_zmultiples_nsmul_iff {G : Type u_1} [AddGroup G] {g : G} {k : ℕ} : g ∈ AddSubgroup.zmultiples (k • g) ↔ k.gcd (addOrderOf g) = 1

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

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

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

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

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

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

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

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

noncomputable def zpowersEquivZPowers {G : Type u_1} [Group G] {x 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 ⋯).symm.trans ((finCongr h).trans (finEquivZPowers ⋯))

noncomputable def zmultiplesEquivZMultiples {G : Type u_1} [AddGroup G] {x 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 ⋯).symm.trans ((finCongr h).trans (finEquivZMultiples ⋯))

@[simp]

theorem zpowersEquivZPowers_apply {G : Type u_1} [Group G] {x y : G} [Finite G] (h : orderOf x = orderOf y) (n : ℕ) : (zpowersEquivZPowers h) ⟨x ^ n, ⋯⟩ = ⟨y ^ n, ⋯⟩

@[simp]

theorem zmultiples_equiv_zmultiples_apply {G : Type u_1} [AddGroup G] {x y : G} [Finite G] (h : addOrderOf x = addOrderOf y) (n : ℕ) : (zmultiplesEquivZMultiples h) ⟨n • x, ⋯⟩ = ⟨n • y, ⋯⟩

theorem Subgroup.closure_toSubmonoid_of_finite {G : Type u_1} [Group G] [Finite G] {s : Set G} : (closure s).toSubmonoid = Submonoid.closure s

See Subgroup.closure_toSubmonoid_of_isOfFinOrder for a version with weaker assumptions.

theorem AddSubgroup.closure_toAddSubmonoid_of_finite {G : Type u_1} [AddGroup G] [Finite G] {s : Set G} : (closure s).toAddSubmonoid = AddSubmonoid.closure s

See AddSubgroup.closure_toAddSubmonoid_of_isOfFinOrder for a version with weaker assumptions.

theorem Fintype.card_zpowers {G : Type u_1} [Group G] [Fintype G] {x : G} : card ↥(Subgroup.zpowers x) = orderOf x

See also Nat.card_zpowers.

theorem Fintype.card_zmultiples {G : Type u_1} [AddGroup G] [Fintype G] {x : G} : card ↥(AddSubgroup.zmultiples x) = addOrderOf x

See also Nat.card_zmultiples.

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 ↥(Subgroup.zpowers a) ≤ k

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 ↥(AddSubgroup.zmultiples a) ≤ k

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

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

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

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

theorem Subgroup.orderOf_dvd_natCard {G : Type u_6} [Group G] (s : Subgroup G) {x : G} (hx : x ∈ s) : orderOf x ∣ Nat.card ↥s

theorem AddSubgroup.addOrderOf_dvd_natCard {G : Type u_6} [AddGroup G] (s : AddSubgroup G) {x : G} (hx : x ∈ s) : addOrderOf x ∣ Nat.card ↥s

theorem Subgroup.orderOf_le_card {G : Type u_6} [Group G] (s : Subgroup G) (hs : (↑s).Finite) {x : G} (hx : x ∈ s) : orderOf x ≤ Nat.card ↥s

theorem AddSubgroup.addOrderOf_le_card {G : Type u_6} [AddGroup G] (s : AddSubgroup G) (hs : (↑s).Finite) {x : G} (hx : x ∈ s) : addOrderOf x ≤ Nat.card ↥s

theorem Submonoid.orderOf_le_card {G : Type u_6} [Group G] (s : Submonoid G) (hs : (↑s).Finite) {x : G} (hx : x ∈ s) : orderOf x ≤ Nat.card ↥s

theorem AddSubmonoid.addOrderOf_le_card {G : Type u_6} [AddGroup G] (s : AddSubmonoid G) (hs : (↑s).Finite) {x : G} (hx : x ∈ s) : addOrderOf x ≤ Nat.card ↥s

@[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_6} [AddGroup G] {x : G} : Nat.card G • x = 0

@[simp]

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

@[simp]

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

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

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

theorem Subgroup.pow_relIndex_mem {G : Type u_6} [Group G] (H : Subgroup G) [H.Normal] {K : Subgroup G} {g : G} (hg : g ∈ K) : g ^ H.relIndex K ∈ H

theorem AddSubgroup.nsmul_relIndex_mem {G : Type u_6} [AddGroup G] (H : AddSubgroup G) [H.Normal] {K : AddSubgroup G} {g : G} (hg : g ∈ K) : H.relIndex K • g ∈ H

@[simp]

theorem pow_mod_card {G : Type u_1} [Group G] [Fintype G] (a : G) (n : ℕ) : a ^ (n % Fintype.card G) = a ^ n

@[simp]

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

@[simp]

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

@[simp]

theorem mod_card_zsmul {G : Type u_1} [AddGroup G] [Fintype G] (a : G) (n : ℤ) : (n % ↑(Fintype.card G)) • a = n • a

@[simp]

theorem pow_mod_natCard {G : Type u_6} [Group G] (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n

@[simp]

theorem mod_natCard_nsmul {G : Type u_6} [AddGroup G] (a : G) (n : ℕ) : (n % Nat.card G) • a = n • a

@[simp]

theorem zpow_mod_natCard {G : Type u_6} [Group G] (a : G) (n : ℤ) : a ^ (n % ↑(Nat.card G)) = a ^ n

@[simp]

theorem mod_natCard_zsmul {G : Type u_6} [AddGroup G] (a : G) (n : ℤ) : (n % ↑(Nat.card G)) • a = n • a

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

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

Equations

• powCoprime h = { toFun := fun (g : G) => g ^ n, invFun := fun (g : G) => g ^ (Nat.card G).gcdB n, left_inv := ⋯, right_inv := ⋯ }

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

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

Equations

• nsmulCoprime h = { toFun := fun (g : G) => n • g, invFun := fun (g : G) => (Nat.card G).gcdB n • g, left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

theorem Nat.Coprime.pow_left_bijective {n : ℕ} {G : Type u_6} [Group G] (hn : (Nat.card G).Coprime n) : Function.Bijective fun (x : G) => x ^ n

theorem Nat.Coprime.nsmul_right_bijective {n : ℕ} {G : Type u_6} [AddGroup G] (hn : (Nat.card G).Coprime n) : Function.Bijective fun (x : G) => n • x

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

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

theorem smul_eq_of_le_smul {G : Type u_6} [Group G] [Finite G] {α : Type u_7} [PartialOrder α] {g : G} {a : α} [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : a ≤ g • a) : g • a = a

theorem smul_eq_of_smul_le {G : Type u_6} [Group G] [Finite G] {α : Type u_7} [PartialOrder α] {g : G} {a : α} [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : g • a ≤ a) : g • a = a

def submonoidOfIdempotent {M : Type u_6} [LeftCancelMonoid M] [Finite 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

• submonoidOfIdempotent S hS1 hS2 = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯ }

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

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

Equations

• addSubmonoidOfIdempotent S hS1 hS2 = { carrier := S, add_mem' := ⋯, zero_mem' := ⋯ }

def subgroupOfIdempotent {G : Type u_6} [Group G] [Finite 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

• subgroupOfIdempotent S hS1 hS2 = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

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

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

Equations

• addSubgroupOfIdempotent S hS1 hS2 = { carrier := S, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

def powCardSubgroup {G : Type u_6} [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

• powCardSubgroup S hS = subgroupOfIdempotent (S ^ Fintype.card G) ⋯ ⋯

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

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

Equations

• smulCardAddSubgroup S hS = addSubgroupOfIdempotent (Fintype.card G • S) ⋯ ⋯

@[simp]

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

@[simp]

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

theorem IsOfFinOrder.eq_one {G : Type u_1} [Semiring G] [LinearOrder G] [IsStrictOrderedRing G] {a : G} (ha₀ : 0 ≤ a) (ha : IsOfFinOrder a) : a = 1

theorem IsOfFinOrder.eq_neg_one {G : Type u_1} [Ring G] [LinearOrder G] [IsStrictOrderedRing G] {a : G} (ha₀ : a ≤ 0) (ha : IsOfFinOrder a) : a = -1

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

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

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

theorem Prod.addOrderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] (x : α × β) : addOrderOf x = (addOrderOf x.1).lcm (addOrderOf x.2)

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

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

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

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

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

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

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

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

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

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

theorem IsOfFinOrder.prod_iff {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {x : α × β} : IsOfFinOrder x ↔ IsOfFinOrder x.1 ∧ IsOfFinOrder x.2

theorem IsOfFinAddOrder.prod_iff {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {x : α × β} : IsOfFinAddOrder x ↔ IsOfFinAddOrder x.1 ∧ IsOfFinAddOrder x.2

theorem Prod.orderOf_mk {α : Type u_4} {β : Type u_5} [Monoid α] [Monoid β] {a : α} {b : β} : orderOf (a, b) = (orderOf a).lcm (orderOf b)

theorem Prod.addOrderOf_mk {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] {a : α} {b : β} : addOrderOf (a, b) = (addOrderOf a).lcm (addOrderOf b)

theorem Pi.orderOf_eq_sInf {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → Monoid (α i)] (x : (i : ι) → α i) : orderOf x = sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), orderOf (x i) ∣ n}

theorem Pi.addOrderOf_eq_sInf {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → AddMonoid (α i)] (x : (i : ι) → α i) : addOrderOf x = sInf {n : ℕ | n > 0 ∧ ∀ (i : ι), addOrderOf (x i) ∣ n}

theorem Pi.orderOf {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → Monoid (α i)] [Fintype ι] (x : (i : ι) → α i) : orderOf x = Finset.univ.lcm fun (i : ι) => orderOf (x i)

theorem Pi.addOrderOf {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → AddMonoid (α i)] [Fintype ι] (x : (i : ι) → α i) : addOrderOf x = Finset.univ.lcm fun (i : ι) => addOrderOf (x i)

theorem orderOf_apply_dvd_orderOf {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → Monoid (α i)] {x : (i : ι) → α i} (i : ι) : orderOf (x i) ∣ orderOf x

theorem addOrderOf_apply_dvd_addOrderOf {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → AddMonoid (α i)] {x : (i : ι) → α i} (i : ι) : addOrderOf (x i) ∣ addOrderOf x

theorem IsOfFinOrder.pi {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → Monoid (α i)] {x : (i : ι) → α i} [Finite ι] : (∀ (i : ι), IsOfFinOrder (x i)) → IsOfFinOrder x

theorem IsOfFinAddOrder.pi {ι : Type u_6} {α : ι → Type u_7} [(i : ι) → AddMonoid (α i)] {x : (i : ι) → α i} [Finite ι] : (∀ (i : ι), IsOfFinAddOrder (x i)) → IsOfFinAddOrder x

@[simp]

theorem Nat.cast_card_eq_zero (R : Type u_6) [AddGroupWithOne R] [Fintype R] : ↑(Fintype.card R) = 0

theorem CharP.addOrderOf_one (R : Type u_6) [NonAssocRing R] : CharP R (addOrderOf 1)

theorem charP_of_ne_zero {R : Type u_6} [NonAssocRing R] (p : ℕ) [Fintype R] (hn : Fintype.card R = p) (hR : ∀ i < p, ↑i = 0 → i = 0) : CharP R p

theorem charP_of_prime_pow_injective (R : Type u_6) [Ring R] [Fintype R] (p n : ℕ) [hp : Fact (Nat.Prime p)] (hn : Fintype.card R = p ^ n) (hR : ∀ i ≤ n, ↑p ^ i = 0 → i = n) : CharP R (p ^ n)

theorem SemiconjBy.orderOf_eq {G : Type u_1} [Group G] (a : G) {x y : G} (h : SemiconjBy a x y) : orderOf x = orderOf y

theorem AddSemiconjBy.addOrderOf_eq {G : Type u_1} [AddGroup G] (a : G) {x y : G} (h : AddSemiconjBy a x y) : addOrderOf x = addOrderOf y

theorem orderOf_piMulSingle {ι : Type u_6} [DecidableEq ι] {M : ι → Type u_7} [(i : ι) → Monoid (M i)] (i : ι) (g : M i) : orderOf (Pi.mulSingle i g) = orderOf g