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

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)

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

abbrev isOfFinAddOrder_iff_zsmul_eq_zero.match_1 {G : Type u_1} [AddGroup G] {x : G} (motive : (∃ (n : ℕ), 0 < n ∧ n • x = 0) → Prop) : ∀ (x_1 : ∃ (n : ℕ), 0 < n ∧ n • x = 0), (∀ (n : ℕ) (hn : 0 < n) (hn' : n • x = 0), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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

abbrev isOfFinAddOrder_iff_zsmul_eq_zero.match_2 {G : Type u_1} [AddGroup G] {x : G} (motive : (∃ (n : ℤ), n ≠ 0 ∧ n • x = 0) → Prop) : ∀ (x_1 : ∃ (n : ℤ), n ≠ 0 ∧ n • x = 0), (∀ (n : ℤ) (hn : n ≠ 0) (hn' : n • x = 0), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem isOfFinOrder_iff_zpow_eq_one {G : Type u_6} [Group G] {x : G} : IsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ 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 IsOfFinOrder.pow {G : Type u_1} [Monoid G] {a : G} {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n)

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 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 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) : 0 < Exists.choose ⋯ ∧ Exists.choose ⋯ • x = 0

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

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

@[inline, reducible]

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

• IsOfFinOrder.groupPowers hx = And.casesOn ⋯ fun (hpos : 0 < Exists.choose ⋯) (hx_1 : x ^ Exists.choose ⋯ = 1) => Submonoid.groupPowers hpos hx_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

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

@[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 IsOfFinAddOrder.addOrderOf_pos {G : Type u_1} [AddMonoid G] {x : G} (h : IsOfFinAddOrder x) : 0 < addOrderOf x

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

@[simp]

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

@[simp]

theorem pow_mod_orderOf {G : Type u_1} [Monoid G] (x : G) (n : ℕ) : x ^ (n % orderOf x) = 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_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_injOn_Iio_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} : Set.InjOn (fun (x_1 : ℕ) => x_1 • x) (Set.Iio (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 IsOfFinAddOrder.mem_multiples_iff_mem_range_addOrderOf {G : Type u_1} [AddMonoid G] {x : G} {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.mem_powers_iff_mem_range_orderOf {G : Type u_1} [Monoid G] {x : G} {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.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 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)))

@[deprecated IsOfFinAddOrder.multiples_eq_image_range_addOrderOf]

theorem IsOfFinAddOrder.powers_eq_image_range_orderOf {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)))

Alias of IsOfFinAddOrder.multiples_eq_image_range_addOrderOf.

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

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

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

@[simp]

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

@[simp]

theorem orderOf_submonoid {G : Type u_1} [Monoid G] {H : Submonoid G} (y : ↥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

@[simp]

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

@[simp]

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

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

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

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

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_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_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_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 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 IsOfFinAddOrder.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 IsOfFinOrder.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 Nat.Coprime.addOrderOf_nsmul {G : Type u_1} [AddMonoid G] {y : G} {m : ℕ} (h : Nat.Coprime (addOrderOf y) m) : addOrderOf (m • y) = addOrderOf y

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

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.natCard_powers_le_orderOf {G : Type u_1} [Monoid G] {a : G} (ha : IsOfFinOrder a) : Nat.card ↑↑(Submonoid.powers a) ≤ orderOf a

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

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

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_1 : ∃ (k : ℕ), addOrderOf x = p ^ k), (∀ (k : ℕ) (hk : addOrderOf x = p ^ k), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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

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_1 : ∃ (m : ℕ), p ^ m • x = 0), (∀ (w : ℕ) (hm : p ^ w • x = 0), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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 : G | ¬IsOfFinAddOrder y}

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

abbrev finEquivMultiples.match_3 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (motive : ↥(AddSubmonoid.multiples x) → Prop) : ∀ (x_1 : ↥(AddSubmonoid.multiples x)), (∀ (i : ℕ), motive { val := (fun (x_2 : ℕ) => x_2 • x) i, property := ⋯ }) → motive x_1

Equations

• ⋯ = ⋯

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

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

Equations

• ⋯ = ⋯

noncomputable def finEquivMultiples {G : Type u_1} [AddLeftCancelMonoid 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 x hx = Equiv.ofBijective (fun (n : Fin (addOrderOf x)) => { val := ↑n • x, property := ⋯ }) ⋯

theorem finEquivMultiples.proof_2 {G : Type u_1} [AddLeftCancelMonoid G] (x : G) (hx : IsOfFinAddOrder x) : (Function.Injective fun (n : Fin (addOrderOf x)) => { val := ↑n • x, property := ⋯ }) ∧ Function.Surjective fun (n : Fin (addOrderOf x)) => { val := ↑n • x, property := ⋯ }

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

Equations

• ⋯ = ⋯

noncomputable def finEquivPowers {G : Type u_1} [LeftCancelMonoid 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 x hx = Equiv.ofBijective (fun (n : Fin (orderOf x)) => { val := x ^ ↑n, property := ⋯ }) ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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 Nat.card_submonoidPowers {G : Type u_1} [LeftCancelMonoid G] {a : G} : Nat.card ↥(Submonoid.powers a) = orderOf a

See also orderOf_eq_card_powers.

@[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 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 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 IsOfFinAddOrder.of_neg {G : Type u_1} [AddGroup G] {x : G} : IsOfFinAddOrder (-x) → IsOfFinAddOrder x

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

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 AddSubgroup.addOrderOf_coe {G : Type u_1} [AddGroup G] {H : AddSubgroup G} (a : ↥H) : addOrderOf ↑a = addOrderOf a

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

@[simp]

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

@[simp]

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

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

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

@[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.mem_multiples_iff_mem_zmultiples {G : Type u_1} [AddGroup G] {x : G} {y : G} (hx : IsOfFinAddOrder x) : y ∈ AddSubmonoid.multiples x ↔ y ∈ AddSubgroup.zmultiples x

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem IsOfFinOrder.mem_powers_iff_mem_zpowers {G : Type u_1} [Group G] {x : G} {y : G} (hx : IsOfFinOrder x) : y ∈ Submonoid.powers x ↔ y ∈ 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.powers_eq_zpowers {G : Type u_1} [Group G] {x : G} (hx : IsOfFinOrder x) : ↑(Submonoid.powers x) = ↑(Subgroup.zpowers x)

theorem IsOfFinAddOrder.mem_zmultiples_iff_mem_range_addOrderOf {G : Type u_1} [AddGroup G] {x : G} {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 IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf {G : Type u_1} [Group G] {x : G} {y : G} [DecidableEq G] (hx : IsOfFinOrder x) : y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun (x_1 : ℕ) => x ^ x_1) (Finset.range (orderOf x))

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 x hx = (finEquivMultiples x hx).trans (Equiv.Set.ofEq ⋯)

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 x hx = (finEquivPowers x hx).trans (Equiv.Set.ofEq ⋯)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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.filter (fun (x : G) => addOrderOf x = m) Finset.univ).card) = (Finset.filter (fun (x : G) => n • x = 0) Finset.univ).card

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_1 : addOrderOf x ∣ n), (∀ (m : ℕ) (hm : n = addOrderOf x * m), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

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.filter (fun (x : G) => orderOf x = m) Finset.univ).card) = (Finset.filter (fun (x : G) => x ^ n = 1) Finset.univ).card

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 isOfFinAddOrder_of_finite {G : Type u_1} [AddLeftCancelMonoid G] [Finite G] (x : G) : IsOfFinAddOrder x

theorem isOfFinOrder_of_finite {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 IsOfFinAddOrder.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 IsOfFinOrder.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] [Finite G] {n : ℕ} (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] [Finite G] {n : ℕ} (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] [Finite G] {x : G} {y : G} [DecidableEq G] : y ∈ AddSubmonoid.multiples x ↔ y ∈ Finset.image (fun (x_1 : ℕ) => x_1 • x) (Finset.range (addOrderOf x))

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

theorem mem_powers_iff_mem_zpowers {G : Type u_1} [Group G] [Finite G] {x : G} {y : 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] [Finite G] {x : G} {y : G} [DecidableEq G] : y ∈ AddSubgroup.zmultiples x ↔ y ∈ Finset.image (fun (x_1 : ℕ) => x_1 • x) (Finset.range (addOrderOf x))

theorem mem_zpowers_iff_mem_range_orderOf {G : Type u_1} [Group G] [Finite G] {x : G} {y : G} [DecidableEq G] : y ∈ Subgroup.zpowers x ↔ y ∈ Finset.image (fun (x_1 : ℕ) => x ^ x_1) (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 def zmultiplesEquivZMultiples {G : Type u_1} [AddGroup G] [Finite G] {x : G} {y : 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 ⋯))

theorem zmultiplesEquivZMultiples.proof_1 {G : Type u_1} [AddGroup G] [Finite G] {x : G} : IsOfFinAddOrder x

theorem zmultiplesEquivZMultiples.proof_2 {G : Type u_1} [AddGroup G] [Finite G] {y : G} : IsOfFinAddOrder y

noncomputable def zpowersEquivZPowers {G : Type u_1} [Group G] [Finite G] {x : G} {y : 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] [Finite G] {x : G} {y : G} (h : addOrderOf x = addOrderOf y) (n : ℕ) : (zmultiplesEquivZMultiples h) { val := n • x, property := ⋯ } = { val := n • y, property := ⋯ }

@[simp]

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

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

See also Nat.card_subgroup.

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

See also Nat.card_addSubgroupZPowers.

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 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 addOrderOf_dvd_card {G : Type u_1} [AddGroup G] [Fintype G] {x : G} : addOrderOf x ∣ Fintype.card G

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

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

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

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

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

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

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

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

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

@[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] [Fintype G] {x : G} : Fintype.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

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

@[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 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_zsmul {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_natCard_nsmul {G : Type u_1} [AddGroup G] (a : G) (n : ℕ) : (n % Nat.card G) • a = n • a

@[simp]

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

@[simp]

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

@[simp]

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

theorem nsmulCoprime.proof_1 {n : ℕ} {G : Type u_1} [AddGroup G] (h : Nat.Coprime (Nat.card G) n) (g : G) : (fun (g : G) => Nat.gcdB (Nat.card G) n • g) ((fun (g : G) => n • g) g) = 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

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

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

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

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

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 Nat.Coprime.nsmul_right_bijective {G : Type u_1} [AddGroup G] {n : ℕ} (hn : Nat.Coprime (Nat.card G) n) : Function.Bijective fun (x : G) => n • x

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

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

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

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)) = Set.toFinset ↑(AddSubgroup.zmultiples 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)) = Set.toFinset ↑(Subgroup.zpowers x)

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

abbrev gcd_nsmul_card_eq_zero_iff.match_1 {G : Type u_1} [Fintype G] {n : ℕ} (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 ⋯) → motive x

Equations

• ⋯ = ⋯

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

theorem addSubmonoidOfIdempotent.proof_3 {M : Type u_1} [AddLeftCancelMonoid M] [Finite M] (S : Set M) (hS1 : Set.Nonempty S) (hS2 : S + S = S) (pow_mem : ∀ a ∈ S, ∀ (n : ℕ), (n + 1) • a ∈ S) : 0 ∈ { carrier := S, add_mem' := ⋯ }.carrier

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] [Finite 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

• addSubmonoidOfIdempotent S hS1 hS2 = let_fun pow_mem := ⋯; { toAddSubsemigroup := { carrier := S, add_mem' := ⋯ }, zero_mem' := ⋯ }

theorem addSubmonoidOfIdempotent.proof_2 {M : Type u_1} [AddLeftCancelMonoid M] (S : Set M) (hS2 : S + S = S) : ∀ {a b : M}, a ∈ S → b ∈ S → a + b ∈ S

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

• submonoidOfIdempotent S hS1 hS2 = let_fun pow_mem := ⋯; { toSubsemigroup := { carrier := S, mul_mem' := ⋯ }, one_mem' := ⋯ }

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

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

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

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

• addSubgroupOfIdempotent S hS1 hS2 = let __src := addSubmonoidOfIdempotent S hS1 hS2; { toAddSubmonoid := { toAddSubsemigroup := { carrier := S, add_mem' := ⋯ }, zero_mem' := ⋯ }, neg_mem' := ⋯ }

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

• subgroupOfIdempotent S hS1 hS2 = let __src := submonoidOfIdempotent S hS1 hS2; { toSubmonoid := { toSubsemigroup := { carrier := S, mul_mem' := ⋯ }, one_mem' := ⋯ }, inv_mem' := ⋯ }

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

theorem smulCardAddSubgroup.proof_3 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (one_mem : 0 ∈ Fintype.card G • S) : Fintype.card G • S + Fintype.card G • S = Fintype.card G • S

theorem smulCardAddSubgroup.proof_2 {G : Type u_1} [AddGroup G] [Fintype G] (S : Set G) (one_mem : 0 ∈ Fintype.card G • S) : ∃ (x : G), x ∈ Fintype.card G • S

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

• smulCardAddSubgroup S hS = let_fun one_mem := ⋯; addSubgroupOfIdempotent (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

• powCardSubgroup S hS = let_fun one_mem := ⋯; subgroupOfIdempotent (S ^ Fintype.card G) ⋯ ⋯

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

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

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.addOrderOf {α : Type u_4} {β : Type u_5} [AddMonoid α] [AddMonoid β] (x : α × β) : addOrderOf x = Nat.lcm (addOrderOf x.1) (addOrderOf x.2)

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

@[deprecated Prod.addOrderOf]

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

Alias of Prod.addOrderOf.

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

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

@[deprecated addOrderOf_fst_dvd_addOrderOf]

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

Alias of addOrderOf_fst_dvd_addOrderOf.

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

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

@[deprecated addOrderOf_snd_dvd_addOrderOf]

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

Alias of addOrderOf_snd_dvd_addOrderOf.

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

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

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

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

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)