Mathlib.GroupTheory.OrderOfElement

isPeriodicPt_mul_iff_pow_eq_one theorem

(x : G) : IsPeriodicPt (x * ·) n 1 ↔ x ^ n = 1

Full source

@[to_additive]
theorem isPeriodicPt_mul_iff_pow_eq_one (x : G) : IsPeriodicPtIsPeriodicPt (x * ·) n 1 ↔ x ^ n = 1 := by
  rw [IsPeriodicPt, IsFixedPt, mul_left_iterate]; beta_reduce; rw [mul_one]

Periodicity of Left Multiplication and Power Identity: $x^n = 1$

Informal description

For any element $x$ in a group $G$ and any natural number $n$, the point $1$ is a periodic point of the left multiplication map by $x$ with period $n$ if and only if $x^n = 1$.

IsOfFinOrder definition

(x : G) : Prop

Full source

/-- `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`. -/
@[to_additive "`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`."]
def IsOfFinOrder (x : G) : Prop :=
  (1 : G) ∈ periodicPts (x * ·)

Finite order of a monoid element

Informal description

An element $ x $ of a monoid $ G $ is said to be of finite order if there exists a positive integer $ n $ such that $ x^n = 1 $, where $ 1 $ is the identity element of $ G $.

isOfFinAddOrder_ofMul_iff theorem

: IsOfFinAddOrder (Additive.ofMul x) ↔ IsOfFinOrder x

Full source

theorem isOfFinAddOrder_ofMul_iff : IsOfFinAddOrderIsOfFinAddOrder (Additive.ofMul x) ↔ IsOfFinOrder x :=
  Iff.rfl

Equivalence of Finite Order in Additive and Multiplicative Monoids

Informal description

For any element $x$ in a multiplicative monoid, the additive version of $x$ (denoted $\text{Additive.ofMul}\,x$) has finite additive order if and only if $x$ has finite multiplicative order.

isOfFinOrder_ofAdd_iff theorem

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

Full source

theorem isOfFinOrder_ofAdd_iff {α : Type*} [AddMonoid α] {x : α} :
    IsOfFinOrderIsOfFinOrder (Multiplicative.ofAdd x) ↔ IsOfFinAddOrder x := Iff.rfl

Equivalence of Finite Order in Multiplicative and Additive Monoids

Informal description

For any element $x$ in an additive monoid $\alpha$, the multiplicative version of $x$ (denoted $\text{Multiplicative.ofAdd}\,x$) has finite multiplicative order if and only if $x$ has finite additive order.

isOfFinOrder_iff_pow_eq_one theorem

: IsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1

Full source

@[to_additive]
theorem isOfFinOrder_iff_pow_eq_one : IsOfFinOrderIsOfFinOrder x ↔ ∃ n, 0 < n ∧ x ^ n = 1 := by
  simp [IsOfFinOrder, mem_periodicPts, isPeriodicPt_mul_iff_pow_eq_one]

Characterization of Finite Order Elements via Powers of Identity

Informal description

An element $x$ of a monoid $G$ has finite order if and only if there exists a positive integer $n$ such that $x^n = 1$, where $1$ is the identity element of $G$.

isOfFinOrder_iff_zpow_eq_one theorem

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

Full source

@[to_additive]
lemma isOfFinOrder_iff_zpow_eq_one {G} [DivisionMonoid G] {x : G} :
    IsOfFinOrderIsOfFinOrder x ↔ ∃ (n : ℤ), n ≠ 0 ∧ x ^ n = 1 := by
  rw [isOfFinOrder_iff_pow_eq_one]
  refine ⟨fun ⟨n, hn, hn'⟩ ↦ ⟨n, Int.natCast_ne_zero_iff_pos.mpr hn, zpow_natCast x n ▸ hn'⟩,
    fun ⟨n, hn, hn'⟩ ↦ ⟨n.natAbs, Int.natAbs_pos.mpr hn, ?_⟩⟩
  rcases (Int.natAbs_eq_iff (a := n)).mp rfl with h | h
  · rwa [h, zpow_natCast] at hn'
  · rwa [h, zpow_neg, inv_eq_one, zpow_natCast] at hn'

Characterization of finite order elements in division monoids via integer powers

Informal description

Let $G$ be a division monoid and $x \in G$. Then $x$ has finite order if and only if there exists a nonzero integer $n$ such that $x^n = 1$.

not_isOfFinOrder_of_injective_pow theorem

{x : G} (h : Injective fun n : ℕ => x ^ n) : ¬IsOfFinOrder x

Full source

/-- See also `injective_pow_iff_not_isOfFinOrder`. -/
@[to_additive "See also `injective_nsmul_iff_not_isOfFinAddOrder`."]
theorem not_isOfFinOrder_of_injective_pow {x : G} (h : Injective fun n : ℕ => x ^ n) :
    ¬IsOfFinOrder x := by
  simp_rw [isOfFinOrder_iff_pow_eq_one, not_exists, not_and]
  intro n hn_pos hnx
  rw [← pow_zero x] at hnx
  rw [h hnx] at hn_pos
  exact irrefl 0 hn_pos

Injectivity of Powers Implies Infinite Order

Informal description

For any element $x$ in a monoid $G$, if the function $n \mapsto x^n$ is injective on the natural numbers, then $x$ does not have finite order in $G$.

IsOfFinOrder.one theorem

: IsOfFinOrder (1 : G)

Full source

/-- 1 is of finite order in any monoid. -/
@[to_additive (attr := simp) "0 is of finite order in any additive monoid."]
theorem IsOfFinOrder.one : IsOfFinOrder (1 : G) :=
  isOfFinOrder_iff_pow_eq_one.mpr ⟨1, Nat.one_pos, one_pow 1⟩

Identity Element Has Finite Order in a Monoid

Informal description

The identity element $1$ of a monoid $G$ has finite order.

IsOfFinOrder.pow theorem

{n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n)

Full source

@[to_additive]
lemma IsOfFinOrder.pow {n : ℕ} : IsOfFinOrder a → IsOfFinOrder (a ^ n) := by
  simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨m, hm, ha⟩
  exact ⟨m, hm, by simp [pow_right_comm _ n, ha]⟩

Powers of Finite Order Elements Have Finite Order

Informal description

If an element $a$ of a monoid $G$ has finite order, then for any natural number $n$, the power $a^n$ also has finite order.

IsOfFinOrder.of_pow theorem

{n : ℕ} (h : IsOfFinOrder (a ^ n)) (hn : n ≠ 0) : IsOfFinOrder a

Full source

@[to_additive]
lemma IsOfFinOrder.of_pow {n : ℕ} (h : IsOfFinOrder (a ^ n)) (hn : n ≠ 0) : IsOfFinOrder a := by
  rw [isOfFinOrder_iff_pow_eq_one] at *
  rcases h with ⟨m, hm, ha⟩
  exact ⟨n * m, mul_pos hn.bot_lt hm, by rwa [pow_mul]⟩

Finite Order of Power Implies Finite Order of Element

Informal description

For any natural number $n \neq 0$, if the power $a^n$ of an element $a$ in a monoid $G$ has finite order, then $a$ itself has finite order.

isOfFinOrder_pow theorem

{n : ℕ} : IsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0

Full source

@[to_additive (attr := simp)]
lemma isOfFinOrder_pow {n : ℕ} : IsOfFinOrderIsOfFinOrder (a ^ n) ↔ IsOfFinOrder a ∨ n = 0 := by
  rcases Decidable.eq_or_ne n 0 with rfl | hn
  · simp
  · exact ⟨fun h ↦ .inl <| h.of_pow hn, fun h ↦ (h.resolve_right hn).pow⟩

Finite Order of Power Element $\leftrightarrow$ Finite Order of Base or Zero Exponent

Informal description

For any natural number $n$, the power $a^n$ of an element $a$ in a monoid $G$ has finite order if and only if either $a$ has finite order or $n = 0$.

Submonoid.isOfFinOrder_coe theorem

{H : Submonoid G} {x : H} : IsOfFinOrder (x : G) ↔ IsOfFinOrder x

Full source

/-- Elements of finite order are of finite order in submonoids. -/
@[to_additive "Elements of finite order are of finite order in submonoids."]
theorem Submonoid.isOfFinOrder_coe {H : Submonoid G} {x : H} :
    IsOfFinOrderIsOfFinOrder (x : G) ↔ IsOfFinOrder x := by
  rw [isOfFinOrder_iff_pow_eq_one, isOfFinOrder_iff_pow_eq_one]
  norm_cast

Finite Order Preservation in Submonoid Inclusion

Informal description

For any submonoid $H$ of a monoid $G$ and any element $x \in H$, the element $x$ has finite order in $G$ if and only if it has finite order in $H$.

IsConj.isOfFinOrder theorem

(h : IsConj x y) : IsOfFinOrder x → IsOfFinOrder y

Full source

theorem IsConj.isOfFinOrder (h : IsConj x y) : IsOfFinOrder x → IsOfFinOrder y := by
  simp_rw [isOfFinOrder_iff_pow_eq_one]
  rintro ⟨n, n_gt_0, eq'⟩
  exact ⟨n, n_gt_0, by rw [← isConj_one_right, ← eq']; exact h.pow n⟩

Conjugate Elements Have the Same Finite Order Property

Informal description

If two elements $x$ and $y$ in a monoid $G$ are conjugate (i.e., there exists $g \in G$ such that $y = gxg^{-1}$), and $x$ has finite order, then $y$ also has finite order.

MonoidHom.isOfFinOrder theorem

[Monoid H] (f : G →* H) {x : G} (h : IsOfFinOrder x) : IsOfFinOrder <| f x

Full source

/-- The image of an element of finite order has finite order. -/
@[to_additive "The image of an element of finite additive order has finite additive order."]
theorem MonoidHom.isOfFinOrder [Monoid H] (f : G →* H) {x : G} (h : IsOfFinOrder x) :
    IsOfFinOrder <| f x :=
  isOfFinOrder_iff_pow_eq_one.mpr <| by
    obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
    exact ⟨n, npos, by rw [← f.map_pow, hn, f.map_one]⟩

Finite Order Preservation under Monoid Homomorphisms

Informal description

Let $G$ and $H$ be monoids, and let $f : G \to H$ be a monoid homomorphism. If an element $x \in G$ has finite order, then its image $f(x) \in H$ also has finite order.

IsOfFinOrder.apply theorem

 {η : Type*} {Gs : η → Type*} [∀ i, Monoid (Gs i)] {x : ∀ i, Gs i} (h : IsOfFinOrder x) : ∀ i, IsOfFinOrder (x i)

Full source

/-- If a direct product has finite order then so does each component. -/
@[to_additive "If a direct product has finite additive order then so does each component."]
theorem IsOfFinOrder.apply {η : Type*} {Gs : η → Type*} [∀ i, Monoid (Gs i)] {x : ∀ i, Gs i}
    (h : IsOfFinOrder x) : ∀ i, IsOfFinOrder (x i) := by
  obtain ⟨n, npos, hn⟩ := h.exists_pow_eq_one
  exact fun _ => isOfFinOrder_iff_pow_eq_one.mpr ⟨n, npos, (congr_fun hn.symm _).symm⟩

Finite Order of Components in Direct Product of Monoids

Informal description

Let $\{G_i\}_{i \in \eta}$ be a family of monoids and $x = (x_i)_{i \in \eta}$ be an element of their direct product. If $x$ has finite order in the direct product, then for each index $i \in \eta$, the component $x_i$ has finite order in $G_i$.

IsOfFinOrder.groupPowers abbrev

(hx : IsOfFinOrder x) : Group (Submonoid.powers x)

Full source

/-- The submonoid generated by an element is a group if that element has finite order. -/
@[to_additive "The additive submonoid generated by an element is
an additive group if that element has finite order."]
noncomputable abbrev IsOfFinOrder.groupPowers (hx : IsOfFinOrder x) :
    Group (Submonoid.powers x) := by
  obtain ⟨hpos, hx⟩ := hx.exists_pow_eq_one.choose_spec
  exact Submonoid.groupPowers hpos hx

Finite Order Element Generates a Group

Informal description

If an element $x$ of a monoid $G$ has finite order, then the submonoid generated by $x$ forms a group.

orderOf definition

(x : G) : ℕ

Full source

/-- `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. -/
@[to_additive
  "`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."]
noncomputable def orderOf (x : G) : ℕ :=
  minimalPeriod (x * ·) 1

Order of an element in a monoid

Informal description

For an element $ x $ in a monoid $ G $, the order of $ x $, denoted $ \text{orderOf}(x) $, is defined as the smallest positive integer $ n $ such that $ x^n = 1 $. If no such $ n $ exists (i.e., $ x $ has infinite order), then $ \text{orderOf}(x) $ is defined to be 0.

addOrderOf_ofMul_eq_orderOf theorem

(x : G) : addOrderOf (Additive.ofMul x) = orderOf x

Full source

@[simp]
theorem addOrderOf_ofMul_eq_orderOf (x : G) : addOrderOf (Additive.ofMul x) = orderOf x :=
  rfl

Equality of Additive and Multiplicative Orders via `Additive.ofMul`

Informal description

For any element $x$ in a monoid $G$, the additive order of $x$ when viewed in the additive monoid (via `Additive.ofMul`) equals the multiplicative order of $x$ in $G$, i.e., $\text{addOrderOf}(\text{Additive.ofMul}(x)) = \text{orderOf}(x)$.

orderOf_ofAdd_eq_addOrderOf theorem

{α : Type*} [AddMonoid α] (a : α) : orderOf (Multiplicative.ofAdd a) = addOrderOf a

Full source

@[simp]
lemma orderOf_ofAdd_eq_addOrderOf {α : Type*} [AddMonoid α] (a : α) :
    orderOf (Multiplicative.ofAdd a) = addOrderOf a := rfl

Equality of Multiplicative Order and Additive Order via `ofAdd`

Informal description

For any element $a$ in an additive monoid $\alpha$, the order of $a$ in the multiplicative monoid (obtained via `Multiplicative.ofAdd`) equals the additive order of $a$ in $\alpha$, i.e., $\text{orderOf}(\text{ofAdd}(a)) = \text{addOrderOf}(a)$.

IsOfFinOrder.orderOf_pos theorem

(h : IsOfFinOrder x) : 0 < orderOf x

Full source

@[to_additive]
protected lemma IsOfFinOrder.orderOf_pos (h : IsOfFinOrder x) : 0 < orderOf x :=
  minimalPeriod_pos_of_mem_periodicPts h

Positivity of Order for Finite Order Elements

Informal description

If an element $ x $ of a monoid $ G $ has finite order, then its order $ \text{orderOf}(x) $ is positive, i.e., $ \text{orderOf}(x) > 0 $.

pow_orderOf_eq_one theorem

(x : G) : x ^ orderOf x = 1

Full source

@[to_additive addOrderOf_nsmul_eq_zero]
theorem pow_orderOf_eq_one (x : G) : x ^ orderOf x = 1 := by
  convert Eq.trans _ (isPeriodicPt_minimalPeriod (x * ·) 1)
  -- Porting note (https://github.com/leanprover-community/mathlib4/issues/12129): additional beta reduction needed in the middle of the rewrite
  rw [orderOf, mul_left_iterate]; beta_reduce; rw [mul_one]

Element to the Power of its Order Equals Identity

Informal description

For any element $x$ in a monoid $G$, raising $x$ to the power of its order $\text{orderOf}(x)$ yields the identity element, i.e., $x^{\text{orderOf}(x)} = 1$.

orderOf_eq_zero theorem

(h : ¬IsOfFinOrder x) : orderOf x = 0

Full source

@[to_additive]
theorem orderOf_eq_zero (h : ¬IsOfFinOrder x) : orderOf x = 0 := by
  rwa [orderOf, minimalPeriod, dif_neg]

Order of an element is zero when it has infinite order

Informal description

For an element $x$ of a monoid $G$, if $x$ does not have finite order (i.e., there is no positive integer $n$ such that $x^n = 1$), then the order of $x$ is zero.

orderOf_eq_zero_iff theorem

: orderOf x = 0 ↔ ¬IsOfFinOrder x

Full source

@[to_additive]
theorem orderOf_eq_zero_iff : orderOforderOf x = 0 ↔ ¬IsOfFinOrder x :=
  ⟨fun h H ↦ H.orderOf_pos.ne' h, orderOf_eq_zero⟩

Characterization of Zero Order: $\text{orderOf}(x) = 0 \leftrightarrow x$ has infinite order

Informal description

For an element $x$ in a monoid $G$, the order of $x$ is zero if and only if $x$ does not have finite order.

orderOf_eq_zero_iff' theorem

: orderOf x = 0 ↔ ∀ n : ℕ, 0 < n → x ^ n ≠ 1

Full source

@[to_additive]
theorem orderOf_eq_zero_iff' : orderOforderOf x = 0 ↔ ∀ n : ℕ, 0 < n → x ^ n ≠ 1 := by
  simp_rw [orderOf_eq_zero_iff, isOfFinOrder_iff_pow_eq_one, not_exists, not_and]

Characterization of Infinite Order: $\text{orderOf}(x) = 0 \leftrightarrow \forall n > 0, x^n \neq 1$

Informal description

For an element $x$ in a monoid $G$, the order of $x$ is zero if and only if for every positive integer $n$, the $n$-th power of $x$ is not equal to the identity element, i.e., $x^n \neq 1$.

orderOf_eq_iff theorem

{n} (h : 0 < n) : orderOf x = n ↔ x ^ n = 1 ∧ ∀ m, m < n → 0 < m → x ^ m ≠ 1

Full source

@[to_additive]
theorem orderOf_eq_iff {n} (h : 0 < n) :
    orderOforderOf x = n ↔ x ^ n = 1 ∧ ∀ m, m < n → 0 < m → x ^ m ≠ 1 := by
  simp_rw [Ne, ← isPeriodicPt_mul_iff_pow_eq_one, orderOf, minimalPeriod]
  split_ifs with h1
  · classical
    rw [find_eq_iff]
    simp only [h, true_and]
    push_neg
    rfl
  · rw [iff_false_left h.ne]
    rintro ⟨h', -⟩
    exact h1 ⟨n, h, h'⟩

Characterization of Finite Order: $\text{orderOf}(x) = n \leftrightarrow (x^n = 1 \land \forall m \in (0, n), x^m \neq 1)$

Informal description

For a positive integer $n$ and an element $x$ in a monoid $G$, the order of $x$ equals $n$ if and only if $x^n = 1$ and for every positive integer $m < n$, we have $x^m \neq 1$.

orderOf_pos_iff theorem

: 0 < orderOf x ↔ IsOfFinOrder x

Full source

/-- A group element has finite order iff its order is positive. -/
@[to_additive
      "A group element has finite additive order iff its order is positive."]
theorem orderOf_pos_iff : 0 < orderOf x ↔ IsOfFinOrder x := by
  rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]

Positive Order Characterizes Finite Order Elements

Informal description

For an element $x$ in a monoid $G$, the order of $x$ is positive if and only if $x$ has finite order, i.e., there exists a positive integer $n$ such that $x^n = 1$.

IsOfFinOrder.mono theorem

[Monoid β] {y : β} (hx : IsOfFinOrder x) (h : orderOf y ∣ orderOf x) : IsOfFinOrder y

Full source

@[to_additive]
theorem IsOfFinOrder.mono [Monoid β] {y : β} (hx : IsOfFinOrder x) (h : orderOforderOf y ∣ orderOf x) :
    IsOfFinOrder y := by rw [← orderOf_pos_iff] at hx ⊢; exact Nat.pos_of_dvd_of_pos h hx

Finite Order Preservation Under Divisibility

Informal description

Let $G$ and $H$ be monoids, and let $x \in G$ be an element of finite order. If the order of an element $y \in H$ divides the order of $x$, then $y$ also has finite order.

pow_ne_one_of_lt_orderOf theorem

(n0 : n ≠ 0) (h : n < orderOf x) : x ^ n ≠ 1

Full source

@[to_additive]
theorem pow_ne_one_of_lt_orderOf (n0 : n ≠ 0) (h : n < orderOf x) : x ^ n ≠ 1 := fun j =>
  not_isPeriodicPt_of_pos_of_lt_minimalPeriod n0 h ((isPeriodicPt_mul_iff_pow_eq_one x).mpr j)

Non-identity Power for Elements Below Order: $x^n \neq 1$ when $n < \text{orderOf}(x)$

Informal description

For any element $x$ in a monoid $G$ and any natural number $n \neq 0$, if $n$ is strictly less than the order of $x$, then $x^n \neq 1$.

orderOf_le_of_pow_eq_one theorem

(hn : 0 < n) (h : x ^ n = 1) : orderOf x ≤ n

Full source

@[to_additive]
theorem orderOf_le_of_pow_eq_one (hn : 0 < n) (h : x ^ n = 1) : orderOf x ≤ n :=
  IsPeriodicPt.minimalPeriod_le hn (by rwa [isPeriodicPt_mul_iff_pow_eq_one])

Order Bound from Power Identity: $\text{orderOf}(x) \leq n$ if $x^n = 1$

Informal description

For any element $x$ in a monoid $G$ and any positive integer $n$, if $x^n = 1$, then the order of $x$ is less than or equal to $n$, i.e., $\text{orderOf}(x) \leq n$.

orderOf_one theorem

: orderOf (1 : G) = 1

Full source

@[to_additive (attr := simp)]
theorem orderOf_one : orderOf (1 : G) = 1 := by
  rw [orderOf, ← minimalPeriod_id (x := (1 : G)), ← one_mul_eq_id]

Order of Identity Element is One

Informal description

The order of the identity element $1$ in a monoid $G$ is $1$, i.e., $\text{orderOf}(1) = 1$.

orderOf_eq_one_iff theorem

: orderOf x = 1 ↔ x = 1

Full source

@[to_additive (attr := simp) AddMonoid.addOrderOf_eq_one_iff]
theorem orderOf_eq_one_iff : orderOforderOf x = 1 ↔ x = 1 := by
  rw [orderOf, minimalPeriod_eq_one_iff_isFixedPt, IsFixedPt, mul_one]

Order One Equals Identity in Monoid

Informal description

For an element $x$ in a monoid $G$, the order of $x$ is equal to $1$ if and only if $x$ is the identity element, i.e., $\text{orderOf}(x) = 1 \leftrightarrow x = 1$.

pow_mod_orderOf theorem

(x : G) (n : ℕ) : x ^ (n % orderOf x) = x ^ n

Full source

@[to_additive (attr := simp) mod_addOrderOf_nsmul]
lemma pow_mod_orderOf (x : G) (n : ℕ) : x ^ (n % orderOf x) = x ^ n :=
  calc
    x ^ (n % orderOf x) = x ^ (n % orderOf x + orderOf x * (n / orderOf x)) := by
        simp [pow_add, pow_mul, pow_orderOf_eq_one]
    _ = x ^ n := by rw [Nat.mod_add_div]

Exponent Reduction Modulo Order: $x^{n \bmod \text{orderOf}(x)} = x^n$

Informal description

For any element $x$ in a monoid $G$ and any natural number $n$, we have $x^{n \bmod \text{orderOf}(x)} = x^n$, where $\text{orderOf}(x)$ is the order of $x$ (the smallest positive integer $k$ such that $x^k = 1$).

orderOf_dvd_of_pow_eq_one theorem

(h : x ^ n = 1) : orderOf x ∣ n

Full source

@[to_additive]
theorem orderOf_dvd_of_pow_eq_one (h : x ^ n = 1) : orderOforderOf x ∣ n :=
  IsPeriodicPt.minimalPeriod_dvd ((isPeriodicPt_mul_iff_pow_eq_one _).mpr h)

Order Divides Exponent When Power is Identity

Informal description

For an element $x$ in a monoid $G$, if $x^n = 1$ for some natural number $n$, then the order of $x$ divides $n$.

orderOf_dvd_iff_pow_eq_one theorem

{n : ℕ} : orderOf x ∣ n ↔ x ^ n = 1

Full source

@[to_additive]
theorem orderOf_dvd_iff_pow_eq_one {n : ℕ} : orderOforderOf x ∣ norderOf x ∣ n ↔ x ^ n = 1 :=
  ⟨fun h => by rw [← pow_mod_orderOf, Nat.mod_eq_zero_of_dvd h, _root_.pow_zero],
    orderOf_dvd_of_pow_eq_one⟩

Order Divides Exponent if and only if Power is Identity

Informal description

For an element $x$ in a monoid $G$ and a natural number $n$, the order of $x$ divides $n$ if and only if $x^n = 1$.

orderOf_pow_dvd theorem

(n : ℕ) : orderOf (x ^ n) ∣ orderOf x

Full source

@[to_additive addOrderOf_smul_dvd]
theorem orderOf_pow_dvd (n : ℕ) : orderOforderOf (x ^ n) ∣ orderOf x := by
  rw [orderOf_dvd_iff_pow_eq_one, pow_right_comm, pow_orderOf_eq_one, one_pow]

Order of Power Divides Order of Element

Informal description

For any element $x$ in a monoid $G$ and any natural number $n$, the order of $x^n$ divides the order of $x$, i.e., $\text{orderOf}(x^n) \mid \text{orderOf}(x)$.

pow_injOn_Iio_orderOf theorem

: (Set.Iio <| orderOf x).InjOn (x ^ ·)

Full source

@[to_additive]
lemma pow_injOn_Iio_orderOf : (Set.Iio <| orderOf x).InjOn (x ^ ·) := by
  simpa only [mul_left_iterate, mul_one]
    using iterate_injOn_Iio_minimalPeriod (f := (x * ·)) (x := 1)

Injectivity of Power Function Below Order of Element

Informal description

For an element $x$ of finite order in a monoid $G$, the function $n \mapsto x^n$ is injective on the set $\{n \in \mathbb{N} \mid n < \text{orderOf}(x)\}$.

IsOfFinOrder.mem_powers_iff_mem_range_orderOf theorem

[DecidableEq G] (hx : IsOfFinOrder x) : y ∈ Submonoid.powers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·)

Full source

@[to_additive]
protected lemma IsOfFinOrder.mem_powers_iff_mem_range_orderOf [DecidableEq G]
    (hx : IsOfFinOrder x) :
    y ∈ Submonoid.powers xy ∈ Submonoid.powers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
  Finset.mem_range_iff_mem_finset_range_of_mod_eq' hx.orderOf_pos <| pow_mod_orderOf _

Membership in Powers Submonoid via Order Range

Informal description

Let $G$ be a monoid with decidable equality and let $x \in G$ be an element of finite order. For any $y \in G$, $y$ is in the submonoid generated by $x$ if and only if $y$ is equal to $x^k$ for some $k$ in the range $0 \leq k < \text{orderOf}(x)$.

IsOfFinOrder.powers_eq_image_range_orderOf theorem

[DecidableEq G] (hx : IsOfFinOrder x) : (Submonoid.powers x : Set G) = (Finset.range (orderOf x)).image (x ^ ·)

Full source

@[to_additive]
protected lemma IsOfFinOrder.powers_eq_image_range_orderOf [DecidableEq G] (hx : IsOfFinOrder x) :
    (Submonoid.powers x : Set G) = (Finset.range (orderOf x)).image (x ^ ·) :=
  Set.ext fun _ ↦ hx.mem_powers_iff_mem_range_orderOf

Powers Submonoid Characterization via Order Range

Informal description

Let $G$ be a monoid with decidable equality and let $x \in G$ be an element of finite order. Then the submonoid generated by $x$ is equal to the set $\{x^k \mid 0 \leq k < \text{orderOf}(x)\}$.

pow_eq_one_iff_modEq theorem

: x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x]

Full source

@[to_additive]
theorem pow_eq_one_iff_modEq : x ^ n = 1 ↔ n ≡ 0 [MOD orderOf x] := by
  rw [modEq_zero_iff_dvd, orderOf_dvd_iff_pow_eq_one]

Power Equals Identity iff Exponent is Congruent to Zero Modulo Order

Informal description

For an element $x$ in a monoid $G$ and a natural number $n$, the power $x^n$ equals the identity element $1$ if and only if $n$ is congruent to $0$ modulo the order of $x$ (i.e., $n \equiv 0 \pmod{\text{orderOf}(x)}$).

orderOf_map_dvd theorem

{H : Type*} [Monoid H] (ψ : G →* H) (x : G) : orderOf (ψ x) ∣ orderOf x

Full source

@[to_additive]
theorem orderOf_map_dvd {H : Type*} [Monoid H] (ψ : G →* H) (x : G) :
    orderOforderOf (ψ x) ∣ orderOf x := by
  apply orderOf_dvd_of_pow_eq_one
  rw [← map_pow, pow_orderOf_eq_one]
  apply map_one

Order of Homomorphic Image Divides Order of Element

Informal description

Let $G$ and $H$ be monoids, and let $\psi: G \to H$ be a monoid homomorphism. For any element $x \in G$, the order of $\psi(x)$ in $H$ divides the order of $x$ in $G$, i.e., $\text{orderOf}(\psi(x)) \mid \text{orderOf}(x)$.

exists_pow_eq_self_of_coprime theorem

(h : n.Coprime (orderOf x)) : ∃ m : ℕ, (x ^ n) ^ m = x

Full source

@[to_additive]
theorem exists_pow_eq_self_of_coprime (h : n.Coprime (orderOf x)) : ∃ m : ℕ, (x ^ n) ^ m = x := by
  by_cases h0 : orderOf x = 0
  · rw [h0, coprime_zero_right] at h
    exact ⟨1, by rw [h, pow_one, pow_one]⟩
  by_cases h1 : orderOf x = 1
  · exact ⟨0, by rw [orderOf_eq_one_iff.mp h1, one_pow, one_pow]⟩
  obtain ⟨m, h⟩ := exists_mul_emod_eq_one_of_coprime h (one_lt_iff_ne_zero_and_ne_one.mpr ⟨h0, h1⟩)
  exact ⟨m, by rw [← pow_mul, ← pow_mod_orderOf, h, pow_one]⟩

Existence of Coprime Power Iterate Returning to Original Element: $(x^n)^m = x$ for $\gcd(n, \text{orderOf}(x)) = 1$

Informal description

For any element $x$ in a monoid $G$ and any natural number $n$ coprime with the order of $x$ (i.e., $\gcd(n, \text{orderOf}(x)) = 1$), there exists a natural number $m$ such that $(x^n)^m = x$.

orderOf_eq_of_pow_and_pow_div_prime theorem

(hn : 0 < n) (hx : x ^ n = 1) (hd : ∀ p : ℕ, p.Prime → p ∣ n → x ^ (n / p) ≠ 1) : orderOf x = n

Full source

/-- If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `n`,
then `x` has order `n` in `G`. -/
@[to_additive addOrderOf_eq_of_nsmul_and_div_prime_nsmul "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 (hn : 0 < n) (hx : x ^ n = 1)
    (hd : ∀ p : ℕ, p.Prime → p ∣ n → x ^ (n / p) ≠ 1) : orderOf x = n := by
  -- Let `a` be `n/(orderOf x)`, and show `a = 1`
  obtain ⟨a, ha⟩ := exists_eq_mul_right_of_dvd (orderOf_dvd_of_pow_eq_one hx)
  suffices a = 1 by simp [this, ha]
  -- Assume `a` is not one...
  by_contra h
  have a_min_fac_dvd_p_sub_one : a.minFac ∣ n := by
    obtain ⟨b, hb⟩ : ∃ b : ℕ, a = b * a.minFac := exists_eq_mul_left_of_dvd a.minFac_dvd
    rw [hb, ← mul_assoc] at ha
    exact Dvd.intro_left (orderOf x * b) ha.symm
  -- Use the minimum prime factor of `a` as `p`.
  refine hd a.minFac (Nat.minFac_prime h) a_min_fac_dvd_p_sub_one ?_
  rw [← orderOf_dvd_iff_pow_eq_one, Nat.dvd_div_iff_mul_dvd a_min_fac_dvd_p_sub_one, ha, mul_comm,
    Nat.mul_dvd_mul_iff_left (IsOfFinOrder.orderOf_pos _)]
  · exact Nat.minFac_dvd a
  · rw [isOfFinOrder_iff_pow_eq_one]
    exact Exists.intro n (id ⟨hn, hx⟩)

Characterization of Element Order via Prime Power Conditions: $\text{orderOf}(x) = n$ when $x^n = 1$ and $x^{n/p} \neq 1$ for all prime $p \mid n$

Informal description

Let $G$ be a monoid and $x \in G$ an element of finite order. Suppose there exists a positive integer $n$ such that $x^n = 1$, and for every prime factor $p$ of $n$, we have $x^{n/p} \neq 1$. Then the order of $x$ is equal to $n$.

orderOf_eq_orderOf_iff theorem

{H : Type*} [Monoid H] {y : H} : orderOf x = orderOf y ↔ ∀ n : ℕ, x ^ n = 1 ↔ y ^ n = 1

Full source

@[to_additive]
theorem orderOf_eq_orderOf_iff {H : Type*} [Monoid H] {y : H} :
    orderOforderOf x = orderOf y ↔ ∀ n : ℕ, x ^ n = 1 ↔ y ^ n = 1 := by
  simp_rw [← isPeriodicPt_mul_iff_pow_eq_one, ← minimalPeriod_eq_minimalPeriod_iff, orderOf]

Order Equality Criterion via Powers of Identity

Informal description

Let $G$ and $H$ be monoids, and let $x \in G$ and $y \in H$. The order of $x$ equals the order of $y$ if and only if for every natural number $n$, $x^n = 1$ holds if and only if $y^n = 1$ holds.

orderOf_injective theorem

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

Full source

/-- An injective homomorphism of monoids preserves orders of elements. -/
@[to_additive "An injective homomorphism of additive monoids preserves orders of elements."]
theorem orderOf_injective {H : Type*} [Monoid H] (f : G →* H) (hf : Function.Injective f) (x : G) :
    orderOf (f x) = orderOf x := by
  simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]

Injective Homomorphism Preserves Element Order

Informal description

Let $G$ and $H$ be monoids, and let $f: G \to H$ be an injective monoid homomorphism. For any element $x \in G$, the order of $f(x)$ in $H$ equals the order of $x$ in $G$.

MulEquiv.orderOf_eq theorem

{H : Type*} [Monoid H] (e : G ≃* H) (x : G) : orderOf (e x) = orderOf x

Full source

/-- A multiplicative equivalence preserves orders of elements. -/
@[to_additive (attr := simp) "An additive equivalence preserves orders of elements."]
lemma MulEquiv.orderOf_eq {H : Type*} [Monoid H] (e : G ≃* H) (x : G) :
    orderOf (e x) = orderOf x :=
  orderOf_injective e.toMonoidHom e.injective x

Multiplicative Equivalence Preserves Element Order

Informal description

Let $G$ and $H$ be monoids, and let $e: G \to H$ be a multiplicative equivalence (i.e., a bijective monoid homomorphism). For any element $x \in G$, the order of $e(x)$ in $H$ equals the order of $x$ in $G$.

Function.Injective.isOfFinOrder_iff theorem

[Monoid H] {f : G →* H} (hf : Injective f) : IsOfFinOrder (f x) ↔ IsOfFinOrder x

Full source

@[to_additive]
theorem Function.Injective.isOfFinOrder_iff [Monoid H] {f : G →* H} (hf : Injective f) :
    IsOfFinOrderIsOfFinOrder (f x) ↔ IsOfFinOrder x := by
  rw [← orderOf_pos_iff, orderOf_injective f hf x, ← orderOf_pos_iff]

Injective Homomorphism Preserves Finite Order Property

Informal description

Let $G$ and $H$ be monoids, and let $f: G \to H$ be an injective monoid homomorphism. For any element $x \in G$, $f(x)$ has finite order in $H$ if and only if $x$ has finite order in $G$.

orderOf_submonoid theorem

{H : Submonoid G} (y : H) : orderOf (y : G) = orderOf y

Full source

@[to_additive (attr := norm_cast, simp)]
theorem orderOf_submonoid {H : Submonoid G} (y : H) : orderOf (y : G) = orderOf y :=
  orderOf_injective H.subtype Subtype.coe_injective y

Order Preservation in Submonoid: $\text{orderOf}(y) = \text{orderOf}(y)$

Informal description

For any submonoid $H$ of a monoid $G$ and any element $y \in H$, the order of $y$ in $G$ equals the order of $y$ in $H$.

orderOf_units theorem

{y : Gˣ} : orderOf (y : G) = orderOf y

Full source

@[to_additive]
theorem orderOf_units {y : Gˣ} : orderOf (y : G) = orderOf y :=
  orderOf_injective (Units.coeHom G) Units.ext y

Order Preservation in Group of Units: $\text{orderOf}(y) = \text{orderOf}(y)$

Informal description

For any unit $y$ in the group of units $G^\times$ of a monoid $G$, the order of $y$ as an element of $G$ equals the order of $y$ as an element of $G^\times$.

IsOfFinOrder.unit definition

{M} [Monoid M] {x : M} (hx : IsOfFinOrder x) : Mˣ

Full source

/-- If the order of `x` is finite, then `x` is a unit with inverse `x ^ (orderOf x - 1)`. -/
@[to_additive (attr := simps) "If the additive order of `x` is finite, then `x` is an additive
unit with inverse `(addOrderOf x - 1) • x`. "]
noncomputable def IsOfFinOrder.unit {M} [Monoid M] {x : M} (hx : IsOfFinOrder x) : Mˣ :=
  ⟨x, x ^ (orderOf x - 1),
    by rw [← _root_.pow_succ', tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one],
    by rw [← _root_.pow_succ, tsub_add_cancel_of_le (by exact hx.orderOf_pos), pow_orderOf_eq_one]⟩

Unit construction from an element of finite order

Informal description

Given an element $ x $ of finite order in a monoid $ M $, the function constructs a unit (invertible element) of $ M $ with $ x $ as its value and $ x^{\text{orderOf}(x) - 1} $ as its inverse.

IsOfFinOrder.isUnit theorem

{M} [Monoid M] {x : M} (hx : IsOfFinOrder x) : IsUnit x

Full source

@[to_additive]
lemma IsOfFinOrder.isUnit {M} [Monoid M] {x : M} (hx : IsOfFinOrder x) : IsUnit x := ⟨hx.unit, rfl⟩

Elements of Finite Order are Units in a Monoid

Informal description

For any element $x$ of finite order in a monoid $M$, $x$ is a unit (i.e., invertible element) of $M$.

orderOf_pow' theorem

(h : n ≠ 0) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n

Full source

@[to_additive]
theorem orderOf_pow' (h : n ≠ 0) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n := by
  unfold orderOf
  rw [← minimalPeriod_iterate_eq_div_gcd h, mul_left_iterate]

Order of a Power: $\text{orderOf}(x^n) = \text{orderOf}(x) / \gcd(\text{orderOf}(x), n)$ for $n \neq 0$

Informal description

For any element $x$ in a group $G$ and any nonzero natural number $n$, the order of $x^n$ is equal to the order of $x$ divided by the greatest common divisor of the order of $x$ and $n$, i.e., $\text{orderOf}(x^n) = \text{orderOf}(x) / \gcd(\text{orderOf}(x), n)$.

orderOf_pow_of_dvd theorem

{x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ orderOf x) : orderOf (x ^ n) = orderOf x / n

Full source

@[to_additive]
lemma orderOf_pow_of_dvd {x : G} {n : ℕ} (hn : n ≠ 0) (dvd : n ∣ orderOf x) :
    orderOf (x ^ n) = orderOf x / n := by rw [orderOf_pow' _ hn, Nat.gcd_eq_right dvd]

Order of a Power When Exponent Divides Order: $\text{orderOf}(x^n) = \text{orderOf}(x)/n$ for $n \mid \text{orderOf}(x)$

Informal description

For any element $x$ in a group $G$ and any nonzero natural number $n$ that divides the order of $x$, the order of $x^n$ is equal to the order of $x$ divided by $n$, i.e., $\text{orderOf}(x^n) = \text{orderOf}(x)/n$.

orderOf_pow_orderOf_div theorem

{x : G} {n : ℕ} (hx : orderOf x ≠ 0) (hn : n ∣ orderOf x) : orderOf (x ^ (orderOf x / n)) = n

Full source

@[to_additive]
lemma orderOf_pow_orderOf_div {x : G} {n : ℕ} (hx : orderOforderOf x ≠ 0) (hn : n ∣ orderOf x) :
    orderOf (x ^ (orderOf x / n)) = n := by
  rw [orderOf_pow_of_dvd _ (Nat.div_dvd_of_dvd hn), Nat.div_div_self hn hx]
  rw [← Nat.div_mul_cancel hn] at hx; exact left_ne_zero_of_mul hx

Order of Power with Exponent $\text{orderOf}(x)/n$: $\text{orderOf}(x^{\text{orderOf}(x)/n}) = n$

Informal description

For any element $x$ in a monoid $G$ with finite order $\text{orderOf}(x) \neq 0$, and any natural number $n$ dividing $\text{orderOf}(x)$, the order of $x^{\text{orderOf}(x)/n}$ is equal to $n$.

IsOfFinOrder.orderOf_pow theorem

(h : IsOfFinOrder x) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n

Full source

@[to_additive]
protected lemma IsOfFinOrder.orderOf_pow (h : IsOfFinOrder x) :
    orderOf (x ^ n) = orderOf x / gcd (orderOf x) n := by
  unfold orderOf
  rw [← minimalPeriod_iterate_eq_div_gcd' h, mul_left_iterate]

Order of a Power of an Element in Terms of GCD

Informal description

Let $x$ be an element of finite order in a monoid $G$. Then for any natural number $n$, the order of $x^n$ is equal to the order of $x$ divided by the greatest common divisor of the order of $x$ and $n$, i.e., \[ \text{orderOf}(x^n) = \frac{\text{orderOf}(x)}{\gcd(\text{orderOf}(x), n)}. \]

Nat.Coprime.orderOf_pow theorem

(h : (orderOf y).Coprime m) : orderOf (y ^ m) = orderOf y

Full source

@[to_additive]
lemma Nat.Coprime.orderOf_pow (h : (orderOf y).Coprime m) : orderOf (y ^ m) = orderOf y := by
  by_cases hg : IsOfFinOrder y
  · rw [hg.orderOf_pow y m , h.gcd_eq_one, Nat.div_one]
  · rw [m.coprime_zero_left.1 (orderOf_eq_zero hg ▸ h), pow_one]

Order of a Power with Coprime Exponent Equals Original Order

Informal description

Let $y$ be an element of a monoid $G$ with finite order, and let $m$ be a natural number such that $\gcd(\text{orderOf}(y), m) = 1$. Then the order of $y^m$ is equal to the order of $y$, i.e., \[ \text{orderOf}(y^m) = \text{orderOf}(y). \]

IsOfFinOrder.natCard_powers_le_orderOf theorem

(ha : IsOfFinOrder a) : Nat.card (powers a : Set G) ≤ orderOf a

Full source

@[to_additive]
lemma IsOfFinOrder.natCard_powers_le_orderOf (ha : IsOfFinOrder a) :
    Nat.card (powers a : Set G) ≤ orderOf a := by
  classical
  simpa [ha.powers_eq_image_range_orderOf, Finset.card_range, Nat.Iio_eq_range]
    using Finset.card_image_le (s := Finset.range (orderOf a))

Cardinality of Powers Submonoid Bounded by Order of Element

Informal description

For any element $a$ of finite order in a monoid $G$, the cardinality of the submonoid generated by $a$ is at most the order of $a$, i.e., \[ \text{card}(\langle a \rangle) \leq \text{orderOf}(a). \]

IsOfFinOrder.finite_powers theorem

(ha : IsOfFinOrder a) : (powers a : Set G).Finite

Full source

@[to_additive]
lemma IsOfFinOrder.finite_powers (ha : IsOfFinOrder a) : (powers a : Set G).Finite := by
  classical rw [ha.powers_eq_image_range_orderOf]; exact Finset.finite_toSet _

Finiteness of Powers for Elements of Finite Order

Informal description

For any element $a$ of finite order in a monoid $G$, the set of all powers of $a$ is finite.

Commute.orderOf_mul_dvd_lcm theorem

(h : Commute x y) : orderOf (x * y) ∣ Nat.lcm (orderOf x) (orderOf y)

Full source

@[to_additive]
theorem orderOf_mul_dvd_lcm (h : Commute x y) :
    orderOforderOf (x * y) ∣ Nat.lcm (orderOf x) (orderOf y) := by
  rw [orderOf, ← comp_mul_left]
  exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left

Order of Product Divides LCM of Orders for Commuting Elements

Informal description

For any two commuting elements $x$ and $y$ in a monoid $G$, the order of their product $x * y$ divides the least common multiple of the orders of $x$ and $y$. In symbols: $$ \text{orderOf}(x * y) \mid \text{lcm}(\text{orderOf}(x), \text{orderOf}(y)) $$

Commute.orderOf_dvd_lcm_mul theorem

(h : Commute x y) : orderOf y ∣ Nat.lcm (orderOf x) (orderOf (x * y))

Full source

@[to_additive]
theorem orderOf_dvd_lcm_mul (h : Commute x y):
    orderOforderOf y ∣ Nat.lcm (orderOf x) (orderOf (x * y)) := by
  by_cases h0 : orderOf x = 0
  · rw [h0, lcm_zero_left]
    apply dvd_zero
  conv_lhs =>
    rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0),
      _root_.pow_succ, mul_assoc]
  exact
    (((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
      (lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (dvd_lcm_left _ _), dvd_lcm_right _ _⟩)

Order of Element Divides LCM of Orders in Commuting Pair

Informal description

For any two commuting elements $x$ and $y$ in a monoid $G$, the order of $y$ divides the least common multiple of the order of $x$ and the order of their product $x \cdot y$. In symbols: $$\text{orderOf}(y) \mid \text{lcm}(\text{orderOf}(x), \text{orderOf}(x \cdot y))$$

Commute.orderOf_mul_dvd_mul_orderOf theorem

(h : Commute x y) : orderOf (x * y) ∣ orderOf x * orderOf y

Full source

@[to_additive addOrderOf_add_dvd_mul_addOrderOf]
theorem orderOf_mul_dvd_mul_orderOf (h : Commute x y):
    orderOforderOf (x * y) ∣ orderOf x * orderOf y :=
  dvd_trans h.orderOf_mul_dvd_lcm (lcm_dvd_mul _ _)

Order of Product Divides Product of Orders for Commuting Elements

Informal description

For any two commuting elements $x$ and $y$ in a monoid $G$, the order of their product $x \cdot y$ divides the product of their orders. That is, $$\text{orderOf}(x \cdot y) \mid \text{orderOf}(x) \cdot \text{orderOf}(y).$$

Commute.orderOf_mul_eq_mul_orderOf_of_coprime theorem

(h : Commute x y) (hco : (orderOf x).Coprime (orderOf y)) : orderOf (x * y) = orderOf x * orderOf y

Full source

@[to_additive addOrderOf_add_eq_mul_addOrderOf_of_coprime]
theorem orderOf_mul_eq_mul_orderOf_of_coprime (h : Commute x y)
    (hco : (orderOf x).Coprime (orderOf y)) : orderOf (x * y) = orderOf x * orderOf y := by
  rw [orderOf, ← comp_mul_left]
  exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

Order of Product of Commuting Elements with Coprime Orders

Informal description

Let $x$ and $y$ be commuting elements in a monoid $G$ such that the orders of $x$ and $y$ are coprime. Then the order of $x * y$ is equal to the product of the orders of $x$ and $y$, i.e., $$\text{orderOf}(x * y) = \text{orderOf}(x) \cdot \text{orderOf}(y).$$

Commute.isOfFinOrder_mul theorem

(h : Commute x y) (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) : IsOfFinOrder (x * y)

Full source

/-- Commuting elements of finite order are closed under multiplication. -/
@[to_additive "Commuting elements of finite additive order are closed under addition."]
theorem isOfFinOrder_mul (h : Commute x y) (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) :
    IsOfFinOrder (x * y) :=
  orderOf_pos_iff.mp <|
    pos_of_dvd_of_pos h.orderOf_mul_dvd_mul_orderOf <| mul_pos hx.orderOf_pos hy.orderOf_pos

Finite Order of Product for Commuting Elements

Informal description

Let $x$ and $y$ be commuting elements in a monoid $G$. If both $x$ and $y$ have finite order, then their product $x \cdot y$ also has finite order.

Commute.orderOf_mul_eq_right_of_forall_prime_mul_dvd theorem

 (h : Commute x y) (hy : IsOfFinOrder y) (hdvd : ∀ p : ℕ, p.Prime → p ∣ orderOf x → p * orderOf x ∣ orderOf y) :
  orderOf (x * y) = orderOf y

Full source

/-- 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`. -/
@[to_additive addOrderOf_add_eq_right_of_forall_prime_mul_dvd
  "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 orderOf_mul_eq_right_of_forall_prime_mul_dvd (h : Commute x y) (hy : IsOfFinOrder y)
    (hdvd : ∀ p : ℕ, p.Prime → p ∣ orderOf x → p * orderOf x ∣ orderOf y) :
    orderOf (x * y) = orderOf y := by
  have hoy := hy.orderOf_pos
  have hxy := dvd_of_forall_prime_mul_dvd hdvd
  apply orderOf_eq_of_pow_and_pow_div_prime hoy <;> simp only [Ne, ← orderOf_dvd_iff_pow_eq_one]
  · exact h.orderOf_mul_dvd_lcm.trans (lcm_dvd hxy dvd_rfl)
  refine fun p hp hpy hd => hp.ne_one ?_
  rw [← Nat.dvd_one, ← mul_dvd_mul_iff_right hoy.ne', one_mul, ← dvd_div_iff_mul_dvd hpy]
  refine (orderOf_dvd_lcm_mul h).trans (lcm_dvd ((dvd_div_iff_mul_dvd hpy).2 ?_) hd)
  by_cases h : p ∣ orderOf x
  exacts [hdvd p hp h, (hp.coprime_iff_not_dvd.2 h).mul_dvd_of_dvd_of_dvd hpy hxy]

Order of Product Equals Order of $y$ Under Prime Multiplicity Condition

Informal description

Let $x$ and $y$ be commuting elements in a monoid $G$ such that $y$ has finite order. If for every prime $p$ dividing $\text{orderOf}(x)$, we have $p \cdot \text{orderOf}(x)$ divides $\text{orderOf}(y)$, then the order of $x \cdot y$ equals the order of $y$, i.e., $$\text{orderOf}(x \cdot y) = \text{orderOf}(y).$$

orderOf_eq_prime_iff theorem

: orderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1

Full source

@[to_additive]
theorem orderOf_eq_prime_iff : orderOforderOf x = p ↔ x ^ p = 1 ∧ x ≠ 1 := by
  rw [orderOf, minimalPeriod_eq_prime_iff, isPeriodicPt_mul_iff_pow_eq_one, IsFixedPt, mul_one]

Characterization of Prime Order Elements: $\text{orderOf}(x) = p \leftrightarrow x^p = 1 \land x \neq 1$

Informal description

For an element $x$ in a monoid $G$ and a prime natural number $p$, the order of $x$ equals $p$ if and only if $x^p = 1$ and $x$ is not the identity element.

orderOf_eq_prime theorem

(hg : x ^ p = 1) (hg1 : x ≠ 1) : orderOf x = p

Full source

/-- The backward direction of `orderOf_eq_prime_iff`. -/
@[to_additive "The backward direction of `addOrderOf_eq_prime_iff`."]
theorem orderOf_eq_prime (hg : x ^ p = 1) (hg1 : x ≠ 1) : orderOf x = p :=
  orderOf_eq_prime_iff.mpr ⟨hg, hg1⟩

Prime Order Characterization: $x^p = 1 \land x \neq 1 \Rightarrow \text{orderOf}(x) = p$

Informal description

For an element $x$ in a monoid $G$ and a prime natural number $p$, if $x^p = 1$ and $x$ is not the identity element, then the order of $x$ is equal to $p$.

orderOf_eq_prime_pow theorem

(hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) : orderOf x = p ^ (n + 1)

Full source

@[to_additive addOrderOf_eq_prime_pow]
theorem orderOf_eq_prime_pow (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :
    orderOf x = p ^ (n + 1) := by
  apply minimalPeriod_eq_prime_pow <;> rwa [isPeriodicPt_mul_iff_pow_eq_one]

Order of an element is a prime power when its minimal power is a prime power

Informal description

Let $x$ be an element of a monoid $G$ and $p$ be a prime natural number. If $x^{p^n} \neq 1$ but $x^{p^{n+1}} = 1$, then the order of $x$ is $p^{n+1}$.

exists_orderOf_eq_prime_pow_iff theorem

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

Full source

@[to_additive exists_addOrderOf_eq_prime_pow_iff]
theorem exists_orderOf_eq_prime_pow_iff :
    (∃ k : ℕ, orderOf x = p ^ k) ↔ ∃ m : ℕ, x ^ (p : ℕ) ^ m = 1 :=
  ⟨fun ⟨k, hk⟩ => ⟨k, by rw [← hk, pow_orderOf_eq_one]⟩, fun ⟨_, hm⟩ => by
    obtain ⟨k, _, hk⟩ := (Nat.dvd_prime_pow hp.elim).mp (orderOf_dvd_of_pow_eq_one hm)
    exact ⟨k, hk⟩⟩

Characterization of Prime Power Order: $\exists k, \text{orderOf}(x) = p^k \leftrightarrow \exists m, x^{p^m} = 1$

Informal description

For an element $ x $ in a monoid $ G $ and a prime natural number $ p $, there exists a natural number $ k $ such that the order of $ x $ is $ p^k $ if and only if there exists a natural number $ m $ such that $ x^{p^m} = 1 $.

finEquivPowers definition

{x : G} (hx : IsOfFinOrder x) : Fin (orderOf x) ≃ powers x

Full source

/-- The equivalence between `Fin (orderOf x)` and `Submonoid.powers x`, sending `i` to `x ^ i` -/
@[to_additive "The equivalence between `Fin (addOrderOf a)` and
`AddSubmonoid.multiples a`, sending `i` to `i • a`"]
noncomputable def finEquivPowers {x : G} (hx : IsOfFinOrder x) : FinFin (orderOf x) ≃ powers x :=
  Equiv.ofBijective (fun n ↦ ⟨x ^ (n : ℕ), ⟨n, rfl⟩⟩) ⟨fun ⟨_, h₁⟩ ⟨_, h₂⟩ ij ↦
    Fin.ext (pow_injOn_Iio_orderOf h₁ h₂ (Subtype.mk_eq_mk.1 ij)), fun ⟨_, i, rfl⟩ ↦
      ⟨⟨i % orderOf x, mod_lt _ hx.orderOf_pos⟩, Subtype.eq <| pow_mod_orderOf _ _⟩⟩

Bijection between finite exponents and powers of an element

Informal description

Given an element $ x $ of finite order in a monoid $ G $, there is a bijection between the finite set $ \text{Fin}(\text{orderOf}(x)) $ (the canonical type with $ \text{orderOf}(x) $ elements) and the submonoid $ \text{powers}(x) $ generated by $ x $. The bijection maps each natural number $ i $ modulo $ \text{orderOf}(x) $ to the element $ x^i $.

finEquivPowers_apply theorem

{x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)} : finEquivPowers hx n = ⟨x ^ (n : ℕ), n, rfl⟩

Full source

@[to_additive (attr := simp)]
lemma finEquivPowers_apply {x : G} (hx : IsOfFinOrder x) {n : Fin (orderOf x)} :
    finEquivPowers hx n = ⟨x ^ (n : ℕ), n, rfl⟩ := rfl

Application of Bijection Between Finite Exponents and Powers of an Element

Informal description

For an element $x$ of finite order in a monoid $G$, the bijection $\text{finEquivPowers}$ maps a natural number $n$ modulo $\text{orderOf}(x)$ to the element $x^n$ in the submonoid generated by $x$. Specifically, for any $n \in \text{Fin}(\text{orderOf}(x))$, we have $\text{finEquivPowers}(hx)(n) = \langle x^n, n, \text{rfl}\rangle$.

finEquivPowers_symm_apply theorem

 {x : G} (hx : IsOfFinOrder x) (n : ℕ) :
  (finEquivPowers hx).symm ⟨x ^ n, _, rfl⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩

Full source

@[to_additive (attr := simp)]
lemma finEquivPowers_symm_apply {x : G} (hx : IsOfFinOrder x) (n : ℕ) :
    (finEquivPowers hx).symm ⟨x ^ n, _, rfl⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩ := by
  rw [Equiv.symm_apply_eq, finEquivPowers_apply, Subtype.mk_eq_mk, ← pow_mod_orderOf, Fin.val_mk]

Inverse Bijection Between Powers and Exponents Modulo Order

Informal description

For an element $x$ of finite order in a monoid $G$, the inverse of the bijection $\text{finEquivPowers}$ maps the element $x^n$ in the submonoid generated by $x$ to the natural number $n$ modulo $\text{orderOf}(x)$. Specifically, for any natural number $n$, we have $(\text{finEquivPowers}(hx))^{-1}(\langle x^n, \_, \text{rfl}\rangle) = \langle n \bmod \text{orderOf}(x), \text{Nat.mod\_lt}\ \_ hx.\text{orderOf\_pos}\rangle$.

IsOfFinOrder.pow_eq_pow_iff_modEq theorem

: x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Full source

@[to_additive]
theorem IsOfFinOrder.pow_eq_pow_iff_modEq : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x] := by
  wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_le hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [pow_add, (hx.isUnit.pow _).mul_eq_left, pow_eq_one_iff_modEq]
  exact ⟨fun h ↦ Nat.ModEq.add_left _ h, fun h ↦ Nat.ModEq.add_left_cancel' _ h⟩

Power Equality Modulo Order: $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$

Informal description

For an element $x$ of finite order in a monoid $G$ and natural numbers $n$ and $m$, the powers $x^n$ and $x^m$ are equal if and only if $n$ and $m$ are congruent modulo the order of $x$, i.e., $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$.

IsOfFinOrder.pow_inj_mod theorem

{n m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x

Full source

@[to_additive]
lemma IsOfFinOrder.pow_inj_mod {n m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x :=
  hx.pow_eq_pow_iff_modEq

Power Equality via Remainders Modulo Order: $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$

Informal description

For an element $x$ of finite order in a monoid $G$ and natural numbers $n$ and $m$, the powers $x^n$ and $x^m$ are equal if and only if the remainders of $n$ and $m$ modulo the order of $x$ are equal, i.e., $x^n = x^m \leftrightarrow n \bmod \text{orderOf}(x) = m \bmod \text{orderOf}(x)$.

pow_eq_pow_iff_modEq theorem

: x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x]

Full source

@[to_additive]
theorem pow_eq_pow_iff_modEq : x ^ n = x ^ m ↔ n ≡ m [MOD orderOf x] := by
  wlog hmn : m ≤ n generalizing m n
  · rw [eq_comm, ModEq.comm, this (le_of_not_le hmn)]
  obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le hmn
  rw [← mul_one (x ^ m), pow_add, mul_left_cancel_iff, pow_eq_one_iff_modEq]
  exact ⟨fun h => Nat.ModEq.add_left _ h, fun h => Nat.ModEq.add_left_cancel' _ h⟩

Power Equality Modulo Order: $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$

Informal description

For an element $x$ in a monoid $G$ and natural numbers $n$ and $m$, the powers $x^n$ and $x^m$ are equal if and only if $n$ is congruent to $m$ modulo the order of $x$, i.e., $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$.

injective_pow_iff_not_isOfFinOrder theorem

: Injective (fun n : ℕ ↦ x ^ n) ↔ ¬IsOfFinOrder x

Full source

@[to_additive (attr := simp)]
lemma injective_pow_iff_not_isOfFinOrder : InjectiveInjective (fun n : ℕ ↦ x ^ n) ↔ ¬IsOfFinOrder x := by
  refine ⟨fun h => not_isOfFinOrder_of_injective_pow h, fun h n m hnm => ?_⟩
  rwa [pow_eq_pow_iff_modEq, orderOf_eq_zero_iff.mpr h, modEq_zero_iff] at hnm

Injectivity of Powers Characterizes Infinite Order: $n \mapsto x^n$ injective $\leftrightarrow$ $x$ has infinite order

Informal description

For an element $x$ in a monoid $G$, the function $n \mapsto x^n$ is injective on the natural numbers if and only if $x$ does not have finite order.

pow_inj_mod theorem

{n m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x

Full source

@[to_additive]
lemma pow_inj_mod {n m : ℕ} : x ^ n = x ^ m ↔ n % orderOf x = m % orderOf x := pow_eq_pow_iff_modEq

Power Equality Modulo Order Remainder: $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$

Informal description

For an element $x$ in a monoid $G$ and natural numbers $n$ and $m$, the powers $x^n$ and $x^m$ are equal if and only if the remainders of $n$ and $m$ modulo the order of $x$ are equal, i.e., $x^n = x^m \leftrightarrow n \equiv m \pmod{\text{orderOf}(x)}$.

pow_inj_iff_of_orderOf_eq_zero theorem

(h : orderOf x = 0) {n m : ℕ} : x ^ n = x ^ m ↔ n = m

Full source

@[to_additive]
theorem pow_inj_iff_of_orderOf_eq_zero (h : orderOf x = 0) {n m : ℕ} : x ^ n = x ^ m ↔ n = m := by
  rw [pow_eq_pow_iff_modEq, h, modEq_zero_iff]

Injective Powers for Elements of Infinite Order: $x^n = x^m \leftrightarrow n = m$

Informal description

For an element $x$ in a monoid $G$ with infinite order (i.e., $\text{orderOf}(x) = 0$), and for any natural numbers $n$ and $m$, the equality $x^n = x^m$ holds if and only if $n = m$.

infinite_not_isOfFinOrder theorem

{x : G} (h : ¬IsOfFinOrder x) : {y : G | ¬IsOfFinOrder y}.Infinite

Full source

@[to_additive]
theorem infinite_not_isOfFinOrder {x : G} (h : ¬IsOfFinOrder x) :
    { y : G | ¬IsOfFinOrder y }.Infinite := by
  let s := { n | 0 < n }.image fun n : ℕ => x ^ n
  have hs : s ⊆ { y : G | ¬IsOfFinOrder y } := by
    rintro - ⟨n, hn : 0 < n, rfl⟩ (contra : IsOfFinOrder (x ^ n))
    apply h
    rw [isOfFinOrder_iff_pow_eq_one] at contra ⊢
    obtain ⟨m, hm, hm'⟩ := contra
    exact ⟨n * m, mul_pos hn hm, by rwa [pow_mul]⟩
  suffices s.Infinite by exact this.mono hs
  contrapose! h
  have : ¬Injective fun n : ℕ => x ^ n := by
    have := Set.not_injOn_infinite_finite_image (Set.Ioi_infinite 0) (Set.not_infinite.mp h)
    contrapose! this
    exact Set.injOn_of_injective this
  rwa [injective_pow_iff_not_isOfFinOrder, Classical.not_not] at this

Infinite Set of Elements Without Finite Order

Informal description

For any element $x$ in a monoid $G$ that does not have finite order, the set $\{y \in G \mid y \text{ does not have finite order}\}$ is infinite.

finite_powers theorem

: (powers a : Set G).Finite ↔ IsOfFinOrder a

Full source

@[to_additive (attr := simp)]
lemma finite_powers : (powers a : Set G).Finite ↔ IsOfFinOrder a := by
  refine ⟨fun h ↦ ?_, IsOfFinOrder.finite_powers⟩
  obtain ⟨m, n, hmn, ha⟩ := h.exists_lt_map_eq_of_forall_mem (f := fun n : ℕ ↦ a ^ n)
    (fun n ↦ by simp [mem_powers_iff])
  refine isOfFinOrder_iff_pow_eq_one.2 ⟨n - m, tsub_pos_iff_lt.2 hmn, ?_⟩
  rw [← mul_left_cancel_iff (a := a ^ m), ← pow_add, add_tsub_cancel_of_le hmn.le, ha, mul_one]

Finiteness of Powers Set Equivalent to Finite Order Condition

Informal description

For an element $a$ in a monoid $G$, the set of all powers $\{a^n \mid n \in \mathbb{N}\}$ is finite if and only if $a$ has finite order, i.e., there exists a positive integer $n$ such that $a^n = 1$.

infinite_powers theorem

: (powers a : Set G).Infinite ↔ ¬IsOfFinOrder a

Full source

@[to_additive (attr := simp)]
lemma infinite_powers : (powers a : Set G).Infinite ↔ ¬ IsOfFinOrder a := finite_powers.not

Infinite Powers Set iff Element Has Infinite Order

Informal description

For an element $a$ in a monoid $G$, the set of powers $\{a^n \mid n \in \mathbb{N}\}$ is infinite if and only if $a$ does not have finite order (i.e., there exists no positive integer $n$ such that $a^n = 1$).

Nat.card_submonoidPowers theorem

: Nat.card (powers a) = orderOf a

Full source

/-- See also `orderOf_eq_card_powers`. -/
@[to_additive "See also `addOrder_eq_card_multiples`."]
lemma Nat.card_submonoidPowers : Nat.card (powers a) = orderOf a := by
  classical
  by_cases ha : IsOfFinOrder a
  · exact (Nat.card_congr (finEquivPowers ha).symm).trans <| by simp
  · have := (infinite_powers.2 ha).to_subtype
    rw [orderOf_eq_zero ha, Nat.card_eq_zero_of_infinite]

Cardinality of Powers Submonoid Equals Order of Element

Informal description

For an element $a$ in a monoid $G$, the cardinality of the submonoid generated by $a$ (i.e., the set $\{a^n \mid n \in \mathbb{N}\}$) is equal to the order of $a$, denoted $\text{orderOf}(a)$.

isOfFinOrder_inv_iff theorem

{x : G} : IsOfFinOrder x⁻¹ ↔ IsOfFinOrder x

Full source

/-- Inverses of elements of finite order have finite order. -/
@[to_additive (attr := simp) "Inverses of elements of finite additive order
have finite additive order."]
theorem isOfFinOrder_inv_iff {x : G} : IsOfFinOrderIsOfFinOrder x⁻¹ ↔ IsOfFinOrder x := by
  simp [isOfFinOrder_iff_pow_eq_one]

Inverse Element Has Finite Order iff Original Element Does

Informal description

For any element $x$ in a group $G$, the inverse $x^{-1}$ has finite order if and only if $x$ itself has finite order.

orderOf_dvd_iff_zpow_eq_one theorem

: (orderOf x : ℤ) ∣ i ↔ x ^ i = 1

Full source

@[to_additive]
theorem orderOf_dvd_iff_zpow_eq_one : (orderOf x : ℤ) ∣ i(orderOf x : ℤ) ∣ i ↔ x ^ i = 1 := by
  rcases Int.eq_nat_or_neg i with ⟨i, rfl | rfl⟩
  · rw [Int.natCast_dvd_natCast, orderOf_dvd_iff_pow_eq_one, zpow_natCast]
  · rw [dvd_neg, Int.natCast_dvd_natCast, zpow_neg, inv_eq_one, zpow_natCast,
      orderOf_dvd_iff_pow_eq_one]

Order Divides Integer Exponent iff Power is Identity: $\text{orderOf}(x) \mid i \leftrightarrow x^i = 1$

Informal description

For an element $x$ in a group $G$ and an integer $i$, the order of $x$ divides $i$ (as integers) if and only if $x^i = 1$.

orderOf_inv theorem

(x : G) : orderOf x⁻¹ = orderOf x

Full source

@[to_additive (attr := simp)]
theorem orderOf_inv (x : G) : orderOf x⁻¹ = orderOf x := by simp [orderOf_eq_orderOf_iff]

Order of Inverse Equals Order of Element

Informal description

For any element $x$ in a group $G$, the order of the inverse element $x^{-1}$ is equal to the order of $x$, i.e., $\text{orderOf}(x^{-1}) = \text{orderOf}(x)$.

orderOf_dvd_sub_iff_zpow_eq_zpow theorem

{a b : ℤ} : (orderOf x : ℤ) ∣ a - b ↔ x ^ a = x ^ b

Full source

@[to_additive]
theorem orderOf_dvd_sub_iff_zpow_eq_zpow {a b : ℤ} : (orderOf x : ℤ) ∣ a - b(orderOf x : ℤ) ∣ a - b ↔ x ^ a = x ^ b := by
  rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Order Divides Exponent Difference iff Powers Are Equal: $\text{orderOf}(x) \mid (a - b) \leftrightarrow x^a = x^b$

Informal description

For any element $x$ in a group $G$ and integers $a$ and $b$, the order of $x$ divides the difference $a - b$ if and only if $x^a = x^b$.

Subgroup.orderOf_coe theorem

(a : H) : orderOf (a : G) = orderOf a

Full source

@[to_additive (attr := norm_cast)]
lemma orderOf_coe (a : H) : orderOf (a : G) = orderOf a :=
  orderOf_injective H.subtype Subtype.coe_injective _

Order Preservation in Subgroup Inclusion

Informal description

For any element $a$ in a subgroup $H$ of a group $G$, the order of $a$ in $G$ is equal to the order of $a$ in $H$, i.e., $\text{orderOf}(a) = \text{orderOf}(a \text{ as an element of } G)$.

Subgroup.orderOf_mk theorem

(a : G) (ha) : orderOf (⟨a, ha⟩ : H) = orderOf a

Full source

@[to_additive (attr := simp)]
lemma orderOf_mk (a : G) (ha) : orderOf (⟨a, ha⟩ : H) = orderOf a := (orderOf_coe _).symm

Order Preservation in Subgroup Construction

Informal description

For any element $a$ in a group $G$ and a proof $ha$ that $a$ belongs to a subgroup $H$ of $G$, the order of the element $\langle a, ha \rangle$ in $H$ is equal to the order of $a$ in $G$, i.e., $\text{orderOf}(\langle a, ha \rangle) = \text{orderOf}(a)$.

zpow_mod_orderOf theorem

(x : G) (z : ℤ) : x ^ (z % (orderOf x : ℤ)) = x ^ z

Full source

@[to_additive mod_addOrderOf_zsmul]
lemma zpow_mod_orderOf (x : G) (z : ℤ) : x ^ (z % (orderOf x : ℤ)) = x ^ z :=
  calc
    x ^ (z % (orderOf x : ℤ)) = x ^ (z % orderOf x + orderOf x * (z / orderOf x) : ℤ) := by
        simp [zpow_add, zpow_mul, pow_orderOf_eq_one]
    _ = x ^ z := by rw [Int.emod_add_ediv]

Periodicity of Group Element Powers: $x^{z \bmod \text{orderOf}(x)} = x^z$

Informal description

For any element $x$ in a group $G$ and any integer $z$, raising $x$ to the power of $z$ modulo the order of $x$ (interpreted as an integer) is equal to raising $x$ to the power of $z$, i.e., $x^{z \bmod \text{orderOf}(x)} = x^z$.

zpow_pow_orderOf theorem

: (x ^ i) ^ orderOf x = 1

Full source

@[to_additive (attr := simp) zsmul_smul_addOrderOf]
theorem zpow_pow_orderOf : (x ^ i) ^ orderOf x = 1 := by
  by_cases h : IsOfFinOrder x
  · rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]
  · rw [orderOf_eq_zero h, _root_.pow_zero]

Power of Element to Order Equals Identity: $(x^i)^{\text{orderOf}(x)} = 1$

Informal description

For any element $x$ in a monoid $G$ and any integer $i$, raising $x^i$ to the power of the order of $x$ yields the identity element, i.e., $(x^i)^{\text{orderOf}(x)} = 1$.

IsOfFinOrder.zpow theorem

(h : IsOfFinOrder x) {i : ℤ} : IsOfFinOrder (x ^ i)

Full source

@[to_additive]
theorem IsOfFinOrder.zpow (h : IsOfFinOrder x) {i : ℤ} : IsOfFinOrder (x ^ i) :=
  isOfFinOrder_iff_pow_eq_one.mpr ⟨orderOf x, h.orderOf_pos, zpow_pow_orderOf⟩

Finite Order is Preserved under Integer Powers

Informal description

If an element $x$ of a monoid $G$ has finite order, then for any integer $i$, the power $x^i$ also has finite order.

IsOfFinOrder.of_mem_zpowers theorem

(h : IsOfFinOrder x) (h' : y ∈ Subgroup.zpowers x) : IsOfFinOrder y

Full source

@[to_additive]
theorem IsOfFinOrder.of_mem_zpowers (h : IsOfFinOrder x) (h' : y ∈ Subgroup.zpowers x) :
    IsOfFinOrder y := by
  obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h'
  exact h.zpow

Finite Order Inherited by Elements in Cyclic Subgroup

Informal description

If an element $x$ of a group $G$ has finite order and $y$ belongs to the cyclic subgroup generated by $x$, then $y$ also has finite order.

orderOf_dvd_of_mem_zpowers theorem

(h : y ∈ Subgroup.zpowers x) : orderOf y ∣ orderOf x

Full source

@[to_additive]
theorem orderOf_dvd_of_mem_zpowers (h : y ∈ Subgroup.zpowers x) : orderOforderOf y ∣ orderOf x := by
  obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp h
  rw [orderOf_dvd_iff_pow_eq_one]
  exact zpow_pow_orderOf

Order Divisibility in Cyclic Subgroups: $\text{orderOf}(y) \mid \text{orderOf}(x)$ for $y \in \langle x \rangle$

Informal description

For any elements $x$ and $y$ in a group $G$, if $y$ belongs to the cyclic subgroup generated by $x$ (i.e., $y \in \langle x \rangle$), then the order of $y$ divides the order of $x$.

smul_eq_self_of_mem_zpowers theorem

{α : Type*} [MulAction G α] (hx : x ∈ Subgroup.zpowers y) {a : α} (hs : y • a = a) : x • a = a

Full source

theorem smul_eq_self_of_mem_zpowers {α : Type*} [MulAction G α] (hx : x ∈ Subgroup.zpowers y)
    {a : α} (hs : y • a = a) : x • a = a := by
  obtain ⟨k, rfl⟩ := Subgroup.mem_zpowers_iff.mp hx
  rw [← MulAction.toPerm_apply, ← MulAction.toPermHom_apply, MonoidHom.map_zpow _ y k,
    MulAction.toPermHom_apply]
  exact Function.IsFixedPt.perm_zpow (by exact hs) k

Fixed Points under Group Actions in Cyclic Subgroups

Informal description

Let $G$ be a group acting on a type $\alpha$ via multiplication, and let $x, y \in G$ such that $x$ is in the subgroup generated by $y$ (i.e., $x \in \langle y \rangle$). If the action of $y$ on an element $a \in \alpha$ fixes $a$ (i.e., $y \cdot a = a$), then the action of $x$ on $a$ also fixes $a$ (i.e., $x \cdot a = a$).

vadd_eq_self_of_mem_zmultiples theorem

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

Full source

theorem vadd_eq_self_of_mem_zmultiples {α G : Type*} [AddGroup G] [AddAction G α] {x y : G}
    (hx : x ∈ AddSubgroup.zmultiples y) {a : α} (hs : y +ᵥ a = a) : x +ᵥ a = a :=
  @smul_eq_self_of_mem_zpowers (Multiplicative G) _ _ _ α _ hx a hs

Fixed Points under Additive Group Actions in Cyclic Subgroups

Informal description

Let $G$ be an additive group acting on a type $\alpha$, and let $x, y \in G$ such that $x$ is in the subgroup generated by $y$ (i.e., $x \in \langle y \rangle$). If the action of $y$ on an element $a \in \alpha$ fixes $a$ (i.e., $y +ᵥ a = a$), then the action of $x$ on $a$ also fixes $a$ (i.e., $x +ᵥ a = a$).

IsOfFinOrder.mem_powers_iff_mem_zpowers theorem

(hx : IsOfFinOrder x) : y ∈ powers x ↔ y ∈ zpowers x

Full source

@[to_additive]
lemma IsOfFinOrder.mem_powers_iff_mem_zpowers (hx : IsOfFinOrder x) :
    y ∈ powers xy ∈ powers x ↔ y ∈ zpowers x :=
  ⟨fun ⟨n, hn⟩ ↦ ⟨n, by simp_all⟩, fun ⟨i, hi⟩ ↦ ⟨(i % orderOf x).natAbs, by
    dsimp only
    rwa [← zpow_natCast, Int.natAbs_of_nonneg <| Int.emod_nonneg _ <|
      Int.natCast_ne_zero_iff_pos.2 <| hx.orderOf_pos, zpow_mod_orderOf]⟩⟩

Equivalence of Powers and zpowers for Finite Order Elements

Informal description

For an element $x$ of finite order in a monoid $G$, an element $y$ belongs to the multiplicative subsemigroup generated by $x$ if and only if $y$ belongs to the multiplicative subgroup generated by $x$.

IsOfFinOrder.powers_eq_zpowers theorem

(hx : IsOfFinOrder x) : (powers x : Set G) = zpowers x

Full source

@[to_additive]
lemma IsOfFinOrder.powers_eq_zpowers (hx : IsOfFinOrder x) : (powers x : Set G) = zpowers x :=
  Set.ext fun _ ↦ hx.mem_powers_iff_mem_zpowers

Equality of Powers and Integer Powers for Finite Order Elements

Informal description

For an element $x$ of finite order in a monoid $G$, the set of powers of $x$ is equal to the set of integer powers of $x$, i.e., $\{x^n \mid n \in \mathbb{N}\} = \{x^k \mid k \in \mathbb{Z}\}$.

IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf theorem

[DecidableEq G] (hx : IsOfFinOrder x) : y ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·)

Full source

@[to_additive]
lemma IsOfFinOrder.mem_zpowers_iff_mem_range_orderOf [DecidableEq G] (hx : IsOfFinOrder x) :
    y ∈ zpowers xy ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
  hx.mem_powers_iff_mem_zpowers.symm.trans hx.mem_powers_iff_mem_range_orderOf

Membership in Cyclic Subgroup via Order Range

Informal description

Let $G$ be a monoid with decidable equality and let $x \in G$ be an element of finite order. For any $y \in G$, $y$ belongs to the subgroup generated by $x$ if and only if $y = x^k$ for some integer $k$ with $0 \leq k < \text{orderOf}(x)$.

finEquivZPowers definition

(hx : IsOfFinOrder x) : Fin (orderOf x) ≃ zpowers x

Full source

/-- The equivalence between `Fin (orderOf x)` and `Subgroup.zpowers x`, sending `i` to `x ^ i`. -/
@[to_additive "The equivalence between `Fin (addOrderOf a)` and
`Subgroup.zmultiples a`, sending `i` to `i • a`."]
noncomputable def finEquivZPowers (hx : IsOfFinOrder x) :
    FinFin (orderOf x) ≃ zpowers x :=
  (finEquivPowers hx).trans <| Equiv.setCongr hx.powers_eq_zpowers

Bijection between finite exponents and integer powers of an element of finite order

Informal description

Given an element $ x $ of finite order in a monoid $ G $, there is a bijection between the finite set $ \text{Fin}(\text{orderOf}(x)) $ (the canonical type with $ \text{orderOf}(x) $ elements) and the subgroup $ \text{zpowers}(x) $ generated by $ x $. The bijection maps each natural number $ i $ modulo $ \text{orderOf}(x) $ to the element $ x^i $.

finEquivZPowers_apply theorem

(hx : IsOfFinOrder x) {n : Fin (orderOf x)} : finEquivZPowers hx n = ⟨x ^ (n : ℕ), n, zpow_natCast x n⟩

Full source

@[to_additive]
lemma finEquivZPowers_apply (hx : IsOfFinOrder x) {n : Fin (orderOf x)} :
    finEquivZPowers hx n = ⟨x ^ (n : ℕ), n, zpow_natCast x n⟩ := rfl

Image of Finite Exponent under Bijection to Cyclic Subgroup

Informal description

Let $x$ be an element of finite order in a monoid $G$, and let $n$ be a natural number modulo $\text{orderOf}(x)$. Then the bijection $\text{finEquivZPowers}$ maps $n$ to the element $x^n$ in the subgroup generated by $x$.

finEquivZPowers_symm_apply theorem

 (hx : IsOfFinOrder x) (n : ℕ) :
  (finEquivZPowers hx).symm ⟨x ^ n, ⟨n, by simp⟩⟩ = ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩

Full source

@[to_additive]
lemma finEquivZPowers_symm_apply (hx : IsOfFinOrder x) (n : ℕ) :
    (finEquivZPowers hx).symm ⟨x ^ n, ⟨n, by simp⟩⟩ =
    ⟨n % orderOf x, Nat.mod_lt _ hx.orderOf_pos⟩ := by
  rw [finEquivZPowers, Equiv.symm_trans_apply]; exact finEquivPowers_symm_apply _ n

Inverse Bijection Between Integer Powers and Exponents Modulo Order

Informal description

For an element $x$ of finite order in a monoid $G$, the inverse of the bijection $\text{finEquivZPowers}$ maps the element $x^n$ in the subgroup generated by $x$ to the natural number $n$ modulo $\text{orderOf}(x)$. Specifically, for any natural number $n$, we have: \[ (\text{finEquivZPowers}(hx))^{-1}(\langle x^n, \langle n, \text{by simp}\rangle \rangle) = \langle n \bmod \text{orderOf}(x), \text{Nat.mod\_lt}\ \_ hx.\text{orderOf\_pos}\rangle. \]

IsOfFinOrder.mul theorem

(hx : IsOfFinOrder x) (hy : IsOfFinOrder y) : IsOfFinOrder (x * y)

Full source

/-- Elements of finite order are closed under multiplication. -/
@[to_additive "Elements of finite additive order are closed under addition."]
theorem IsOfFinOrder.mul (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) : IsOfFinOrder (x * y) :=
  (Commute.all x y).isOfFinOrder_mul hx hy

Product of Finite Order Elements Has Finite Order

Informal description

Let $x$ and $y$ be elements of a monoid $G$. If both $x$ and $y$ have finite order, then their product $x \cdot y$ also has finite order.

sum_card_orderOf_eq_card_pow_eq_one theorem

[Fintype G] [DecidableEq G] (hn : n ≠ 0) : ∑ m ∈ divisors n, #{x : G | orderOf x = m} = #{x : G | x ^ n = 1}

Full source

@[to_additive]
theorem sum_card_orderOf_eq_card_pow_eq_one [Fintype G] [DecidableEq G] (hn : n ≠ 0) :
    ∑ m ∈ divisors n, #{x : G | orderOf x = m} = #{x : G | x ^ n = 1} := by
  refine (Finset.card_biUnion ?_).symm.trans ?_
  · simp +contextual [Set.PairwiseDisjoint, Set.Pairwise, disjoint_iff, Finset.ext_iff]
  · congr; ext; simp [hn, orderOf_dvd_iff_pow_eq_one]

Sum of Element Counts by Order Equals Count of Elements Satisfying $x^n = 1$

Informal description

Let $G$ be a finite monoid with decidable equality, and let $n$ be a nonzero natural number. The sum of the number of elements in $G$ with order $m$ for each divisor $m$ of $n$ equals the number of elements $x \in G$ such that $x^n = 1$. In other words: \[ \sum_{m \mid n} \#\{x \in G \mid \text{orderOf}(x) = m\} = \#\{x \in G \mid x^n = 1\}. \]

orderOf_le_card_univ theorem

[Fintype G] : orderOf x ≤ Fintype.card G

Full source

@[to_additive]
theorem orderOf_le_card_univ [Fintype G] : orderOf x ≤ Fintype.card G :=
  Finset.le_card_of_inj_on_range (x ^ ·) (fun _ _ ↦ Finset.mem_univ _) pow_injOn_Iio_orderOf

Order of Element Bounded by Group Cardinality

Informal description

For any element $x$ in a finite monoid $G$, the order of $x$ is at most the cardinality of $G$, i.e., $\text{orderOf}(x) \leq |G|$.

orderOf_le_card theorem

[Finite G] : orderOf x ≤ Nat.card G

Full source

@[to_additive]
theorem orderOf_le_card [Finite G] : orderOf x ≤ Nat.card G := by
  obtain ⟨⟩ := nonempty_fintype G
  simpa using orderOf_le_card_univ

Order of Element Bounded by Group Cardinality

Informal description

For any element $x$ in a finite monoid $G$, the order of $x$ is at most the cardinality of $G$, i.e., $\text{orderOf}(x) \leq |G|$.

isOfFinOrder_of_finite theorem

(x : G) : IsOfFinOrder x

Full source

@[to_additive]
lemma isOfFinOrder_of_finite (x : G) : IsOfFinOrder x := by
  by_contra h; exact infinite_not_isOfFinOrder h <| Set.toFinite _

Finite Monoid Elements Have Finite Order

Informal description

For any element $x$ in a finite monoid $G$, $x$ has finite order, i.e., there exists a positive integer $n$ such that $x^n = 1$.

orderOf_pos theorem

(x : G) : 0 < orderOf x

Full source

/-- 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. -/
@[to_additive "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."]
lemma orderOf_pos (x : G) : 0 < orderOf x := (isOfFinOrder_of_finite x).orderOf_pos

Positivity of Element Order in Finite Cancellative Monoids

Informal description

For any element $x$ in a finite cancellative monoid $G$, the order of $x$ is positive, i.e., $\text{orderOf}(x) > 0$.

orderOf_pow theorem

(x : G) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n

Full source

/-- 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. -/
@[to_additive "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 (x : G) : orderOf (x ^ n) = orderOf x / gcd (orderOf x) n :=
  (isOfFinOrder_of_finite _).orderOf_pow ..

Order of a Power: $\text{orderOf}(x^n) = \text{orderOf}(x)/\gcd(\text{orderOf}(x), n)$

Informal description

For any element $x$ in a monoid $G$, the order of $x^n$ is equal to the order of $x$ divided by the greatest common divisor of the order of $x$ and $n$, i.e., \[ \text{orderOf}(x^n) = \frac{\text{orderOf}(x)}{\gcd(\text{orderOf}(x), n)}. \]

mem_powers_iff_mem_range_orderOf theorem

[DecidableEq G] : y ∈ powers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·)

Full source

@[to_additive]
theorem mem_powers_iff_mem_range_orderOf [DecidableEq G] :
    y ∈ powers xy ∈ powers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
  Finset.mem_range_iff_mem_finset_range_of_mod_eq' (orderOf_pos x) <| pow_mod_orderOf _

Membership in Powers Submonoid via Order: $y \in \langle x \rangle \leftrightarrow y = x^n$ for some $0 \leq n < \text{orderOf}(x)$

Informal description

For an element $x$ in a monoid $G$ with decidable equality, an element $y$ belongs to the submonoid generated by $x$ if and only if $y$ is equal to $x^n$ for some $n$ in the range $\{0, \dots, \text{orderOf}(x) - 1\}$.

powersEquivPowers definition

(h : orderOf x = orderOf y) : powers x ≃ powers y

Full source

/-- The equivalence between `Submonoid.powers` of two elements `x, y` of the same order, mapping
  `x ^ i` to `y ^ i`. -/
@[to_additive
  "The equivalence between `Submonoid.multiples` of two elements `a, b` of the same additive order,
  mapping `i • a` to `i • b`."]
noncomputable def powersEquivPowers (h : orderOf x = orderOf y) : powerspowers x ≃ powers y :=
  (finEquivPowers <| isOfFinOrder_of_finite _).symm.trans <|
    (finCongr h).trans <| finEquivPowers <| isOfFinOrder_of_finite _

Equivalence of powers submonoids for elements of the same order

Informal description

Given two elements $ x $ and $ y $ in a finite monoid $ G $ with the same order, there is an equivalence between the submonoids generated by $ x $ and $ y $. Specifically, the equivalence maps $ x^n $ to $ y^n $ for any natural number $ n $.

powersEquivPowers_apply theorem

(h : orderOf x = orderOf y) (n : ℕ) : powersEquivPowers h ⟨x ^ n, n, rfl⟩ = ⟨y ^ n, n, rfl⟩

Full source

@[to_additive (attr := simp)]
theorem powersEquivPowers_apply (h : orderOf x = orderOf y) (n : ℕ) :
    powersEquivPowers h ⟨x ^ n, n, rfl⟩ = ⟨y ^ n, n, rfl⟩ := by
  rw [powersEquivPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivPowers_symm_apply]
  simp [h]

Powers Equivalence Maps Powers to Powers: $\mathrm{powersEquivPowers}(h)(x^n) = y^n$

Informal description

For elements $x$ and $y$ in a finite monoid $G$ with the same order, the equivalence $\mathrm{powersEquivPowers}(h)$ maps the element $\langle x^n, n, \mathrm{rfl}\rangle$ in the submonoid generated by $x$ to the element $\langle y^n, n, \mathrm{rfl}\rangle$ in the submonoid generated by $y$.

orderOf_eq_card_powers theorem

: orderOf x = Fintype.card (powers x : Submonoid G)

Full source

@[to_additive]
lemma orderOf_eq_card_powers : orderOf x = Fintype.card (powers x : Submonoid G) :=
  (Fintype.card_fin (orderOf x)).symm.trans <|
    Fintype.card_eq.2 ⟨finEquivPowers <| isOfFinOrder_of_finite _⟩

Order Equals Cardinality of Generated Submonoid: $\text{orderOf}(x) = |\langle x \rangle|$

Informal description

For any element $x$ in a finite monoid $G$, the order of $x$ is equal to the cardinality of the submonoid generated by $x$, i.e., $\text{orderOf}(x) = |\langle x \rangle|$.

zpow_eq_one_iff_modEq theorem

{n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x]

Full source

@[to_additive]
theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by
  rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]

Power Equals Identity iff Exponent is Congruent to Zero Modulo Order: $x^n = 1 \leftrightarrow n \equiv 0 \pmod{\text{orderOf}(x)}$

Informal description

For an element $x$ in a group $G$ and an integer $n$, the power $x^n$ equals the identity element $1$ if and only if $n$ is congruent to $0$ modulo the order of $x$, i.e., $n \equiv 0 \pmod{\text{orderOf}(x)}$.

zpow_eq_zpow_iff_modEq theorem

{m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x]

Full source

@[to_additive]
theorem zpow_eq_zpow_iff_modEq {m n : ℤ} : x ^ m = x ^ n ↔ m ≡ n [ZMOD orderOf x] := by
  rw [← mul_inv_eq_one, ← zpow_sub, zpow_eq_one_iff_modEq, Int.modEq_iff_dvd, Int.modEq_iff_dvd,
    zero_sub, neg_sub]

Equality of Powers Modulo Order: $x^m = x^n \leftrightarrow m \equiv n \pmod{\text{orderOf}(x)}$

Informal description

For any integers $m$ and $n$, the powers $x^m$ and $x^n$ of an element $x$ in a group $G$ are equal if and only if $m$ and $n$ are congruent modulo the order of $x$, i.e., $x^m = x^n \leftrightarrow m \equiv n \pmod{\text{orderOf}(x)}$.

injective_zpow_iff_not_isOfFinOrder theorem

: (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x

Full source

@[to_additive (attr := simp)]
theorem injective_zpow_iff_not_isOfFinOrder : (Injective fun n : ℤ => x ^ n) ↔ ¬IsOfFinOrder x := by
  refine ⟨?_, fun h n m hnm => ?_⟩
  · simp_rw [isOfFinOrder_iff_pow_eq_one]
    rintro h ⟨n, hn, hx⟩
    exact Nat.cast_ne_zero.2 hn.ne' (h <| by simpa using hx)
  rwa [zpow_eq_zpow_iff_modEq, orderOf_eq_zero_iff.2 h, Nat.cast_zero, Int.modEq_zero_iff] at hnm

Injectivity of Power Function vs. Infinite Order: $n \mapsto x^n$ is injective $\leftrightarrow$ $x$ has infinite order

Informal description

The function $n \mapsto x^n$ from the integers to the group $G$ is injective if and only if the element $x$ does not have finite order.

exists_zpow_eq_one theorem

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

Full source

@[to_additive]
theorem exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (_ : i ≠ 0), x ^ (i : ℤ) = 1 := by
  obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x
  refine ⟨w, Int.natCast_ne_zero.mpr (_root_.ne_of_gt hw1), ?_⟩
  rw [zpow_natCast]
  exact (isPeriodicPt_mul_iff_pow_eq_one _).mp hw2

Existence of Nonzero Integer Power Yielding Identity in a Group

Informal description

For any element $x$ in a group $G$, there exists a nonzero integer $i$ such that $x^i = 1$.

mem_powers_iff_mem_zpowers theorem

: y ∈ powers x ↔ y ∈ zpowers x

Full source

@[to_additive]
lemma mem_powers_iff_mem_zpowers : y ∈ powers xy ∈ powers x ↔ y ∈ zpowers x :=
  (isOfFinOrder_of_finite _).mem_powers_iff_mem_zpowers

Equivalence of Powers and zpowers in a Monoid: $y \in \langle x \rangle \leftrightarrow y \in \langle x \rangle_\mathbb{Z}$

Informal description

For any element $y$ in a monoid $G$, $y$ belongs to the multiplicative subsemigroup generated by $x$ if and only if $y$ belongs to the multiplicative subgroup generated by $x$.

powers_eq_zpowers theorem

(x : G) : (powers x : Set G) = zpowers x

Full source

@[to_additive]
lemma powers_eq_zpowers (x : G) : (powers x : Set G) = zpowers x :=
  (isOfFinOrder_of_finite _).powers_eq_zpowers

Equality of Powers and Integer Powers in a Monoid

Informal description

For any element $x$ in a monoid $G$, the set of powers $\{x^n \mid n \in \mathbb{N}\}$ is equal to the set of integer powers $\{x^k \mid k \in \mathbb{Z}\}$.

mem_zpowers_iff_mem_range_orderOf theorem

[DecidableEq G] : y ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·)

Full source

@[to_additive]
lemma mem_zpowers_iff_mem_range_orderOf [DecidableEq G] :
    y ∈ zpowers xy ∈ zpowers x ↔ y ∈ (Finset.range (orderOf x)).image (x ^ ·) :=
  (isOfFinOrder_of_finite _).mem_zpowers_iff_mem_range_orderOf

Membership in Cyclic Subgroup via Order Range

Informal description

Let $G$ be a monoid with decidable equality and let $x \in G$ be an element of finite order. For any $y \in G$, $y$ belongs to the cyclic subgroup generated by $x$ if and only if $y = x^k$ for some integer $k$ with $0 \leq k < \text{orderOf}(x)$, where $\text{orderOf}(x)$ is the order of $x$.

zpowersEquivZPowers definition

(h : orderOf x = orderOf y) : Subgroup.zpowers x ≃ Subgroup.zpowers y

Full source

/-- The equivalence between `Subgroup.zpowers` of two elements `x, y` of the same order, mapping
  `x ^ i` to `y ^ i`. -/
@[to_additive
  "The equivalence between `Subgroup.zmultiples` of two elements `a, b` of the same additive order,
  mapping `i • a` to `i • b`."]
noncomputable def zpowersEquivZPowers (h : orderOf x = orderOf y) :
    Subgroup.zpowersSubgroup.zpowers x ≃ Subgroup.zpowers y :=
  (finEquivZPowers <| isOfFinOrder_of_finite _).symm.trans <| (finCongr h).trans <|
    finEquivZPowers <| isOfFinOrder_of_finite _

Equivalence between cyclic subgroups of elements with the same order

Informal description

Given two elements $x$ and $y$ in a finite group $G$ with the same order, the function $\mathrm{zpowersEquivZPowers}(h)$ defines an equivalence between the cyclic subgroups $\mathrm{zpowers}(x)$ and $\mathrm{zpowers}(y)$. Specifically, it maps $x^i$ to $y^i$ for each exponent $i$, establishing a bijection between the two subgroups.

zpowersEquivZPowers_apply theorem

 (h : orderOf x = orderOf y) (n : ℕ) : zpowersEquivZPowers h ⟨x ^ n, n, zpow_natCast x n⟩ = ⟨y ^ n, n, zpow_natCast y n⟩

Full source

@[to_additive (attr := simp) zmultiples_equiv_zmultiples_apply]
theorem zpowersEquivZPowers_apply (h : orderOf x = orderOf y) (n : ℕ) :
    zpowersEquivZPowers h ⟨x ^ n, n, zpow_natCast x n⟩ = ⟨y ^ n, n, zpow_natCast y n⟩ := by
  rw [zpowersEquivZPowers, Equiv.trans_apply, Equiv.trans_apply, finEquivZPowers_symm_apply, ←
    Equiv.eq_symm_apply, finEquivZPowers_symm_apply]
  simp [h]

Equivalence of Cyclic Subgroups Maps Powers Correspondingly

Informal description

Given two elements $x$ and $y$ in a finite group $G$ with the same order, the equivalence $\mathrm{zpowersEquivZPowers}(h)$ between the cyclic subgroups generated by $x$ and $y$ maps the element $x^n$ to $y^n$ for any natural number $n$. Specifically, for any $n \in \mathbb{N}$, we have: \[ \mathrm{zpowersEquivZPowers}(h)(\langle x^n, n, \text{zpow\_natCast}\ x\ n\rangle) = \langle y^n, n, \text{zpow\_natCast}\ y\ n\rangle. \]

Fintype.card_zpowers theorem

: Fintype.card (zpowers x) = orderOf x

Full source

/-- See also `Nat.card_zpowers`. -/
@[to_additive "See also `Nat.card_zmultiples`."]
theorem Fintype.card_zpowers : Fintype.card (zpowers x) = orderOf x :=
  (Fintype.card_eq.2 ⟨finEquivZPowers <| isOfFinOrder_of_finite _⟩).symm.trans <|
    Fintype.card_fin (orderOf x)

Cardinality of Cyclic Subgroup Equals Order of Generator

Informal description

For any element $x$ in a finite monoid $G$, the cardinality of the subgroup $\langle x \rangle$ generated by $x$ is equal to the order of $x$, i.e., $|\langle x \rangle| = \text{orderOf}(x)$.

card_zpowers_le theorem

(a : G) {k : ℕ} (k_pos : k ≠ 0) (ha : a ^ k = 1) : Fintype.card (Subgroup.zpowers a) ≤ k

Full source

@[to_additive]
theorem card_zpowers_le (a : G) {k : ℕ} (k_pos : k ≠ 0)
    (ha : a ^ k = 1) : Fintype.card (Subgroup.zpowers a) ≤ k := by
  rw [Fintype.card_zpowers]
  apply orderOf_le_of_pow_eq_one k_pos.bot_lt ha

Cardinality Bound for Cyclic Subgroup: $|\langle a \rangle| \leq k$ when $a^k = 1$

Informal description

For any element $a$ in a finite group $G$ and any positive integer $k$ such that $a^k = 1$, the cardinality of the cyclic subgroup $\langle a \rangle$ is less than or equal to $k$, i.e., $|\langle a \rangle| \leq k$.

orderOf_dvd_card theorem

: orderOf x ∣ Fintype.card G

Full source

@[to_additive]
theorem orderOf_dvd_card : orderOforderOf x ∣ Fintype.card G := by
  classical
    have ft_prod : Fintype ((G ⧸ zpowers x) × zpowers x) :=
      Fintype.ofEquiv G groupEquivQuotientProdSubgroup
    have ft_s : Fintype (zpowers x) := @Fintype.prodRight _ _ _ ft_prod _
    have ft_cosets : Fintype (G ⧸ zpowers x) :=
      @Fintype.prodLeft _ _ _ ft_prod ⟨⟨1, (zpowers x).one_mem⟩⟩
    have eq₁ : Fintype.card G = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
      calc
        Fintype.card G = @Fintype.card _ ft_prod :=
          @Fintype.card_congr _ _ _ ft_prod groupEquivQuotientProdSubgroup
        _ = @Fintype.card _ (@instFintypeProd _ _ ft_cosets ft_s) :=
          congr_arg (@Fintype.card _) <| Subsingleton.elim _ _
        _ = @Fintype.card _ ft_cosets * @Fintype.card _ ft_s :=
          @Fintype.card_prod _ _ ft_cosets ft_s

    have eq₂ : orderOf x = @Fintype.card _ ft_s :=
      calc
        orderOf x = _ := Fintype.card_zpowers.symm
        _ = _ := congr_arg (@Fintype.card _) <| Subsingleton.elim _ _

    exact Dvd.intro (@Fintype.card (G ⧸ Subgroup.zpowers x) ft_cosets) (by rw [eq₁, eq₂, mul_comm])

Order of Element Divides Group Order

Informal description

For any element $ x $ in a finite group $ G $, the order of $ x $ divides the cardinality of $ G $, i.e., $ \text{orderOf}(x) \mid |G| $.

orderOf_dvd_natCard theorem

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

Full source

@[to_additive]
theorem orderOf_dvd_natCard {G : Type*} [Group G] (x : G) : orderOforderOf x ∣ Nat.card G := by
  obtain h | h := fintypeOrInfinite G
  · simp only [Nat.card_eq_fintype_card, orderOf_dvd_card]
  · simp only [card_eq_zero_of_infinite, dvd_zero]

Order of Element Divides Group Cardinality

Informal description

For any element $x$ in a group $G$, the order of $x$ divides the cardinality of $G$ (when $G$ is considered as a type).

Subgroup.orderOf_dvd_natCard theorem

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

Full source

@[to_additive]
nonrec lemma Subgroup.orderOf_dvd_natCard {G : Type*} [Group G] (s : Subgroup G) {x} (hx : x ∈ s) :
  orderOforderOf x ∣ Nat.card s := by simpa using orderOf_dvd_natCard (⟨x, hx⟩ : s)

Order of Element in Subgroup Divides Subgroup Cardinality

Informal description

For any subgroup $s$ of a group $G$ and any element $x \in s$, the order of $x$ divides the cardinality of $s$ (when $s$ is considered as a type).

Subgroup.orderOf_le_card theorem

{G : Type*} [Group G] (s : Subgroup G) (hs : (s : Set G).Finite) {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s

Full source

@[to_additive]
lemma Subgroup.orderOf_le_card {G : Type*} [Group G] (s : Subgroup G) (hs : (s : Set G).Finite)
    {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s :=
  le_of_dvd (Nat.card_pos_iff.2 <| ⟨s.coe_nonempty.to_subtype, hs.to_subtype⟩) <|
    s.orderOf_dvd_natCard hx

Order of Element in Finite Subgroup Bounded by Subgroup Cardinality

Informal description

For any subgroup $s$ of a group $G$ with finite underlying set, and any element $x \in s$, the order of $x$ is less than or equal to the cardinality of $s$ (when $s$ is considered as a type). That is, $\text{orderOf}(x) \leq |s|$.

Submonoid.orderOf_le_card theorem

{G : Type*} [Group G] (s : Submonoid G) (hs : (s : Set G).Finite) {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s

Full source

@[to_additive]
lemma Submonoid.orderOf_le_card {G : Type*} [Group G] (s : Submonoid G) (hs : (s : Set G).Finite)
    {x} (hx : x ∈ s) : orderOf x ≤ Nat.card s := by
  rw [← Nat.card_submonoidPowers]; exact Nat.card_mono hs <| powers_le.2 hx

Order of Element in Finite Submonoid Bounded by Submonoid Cardinality

Informal description

For any submonoid $s$ of a group $G$ with finite underlying set, and any element $x \in s$, the order of $x$ is less than or equal to the cardinality of $s$ (when $s$ is considered as a type). That is, $\text{orderOf}(x) \leq |s|$.

pow_card_eq_one' theorem

{G : Type*} [Group G] {x : G} : x ^ Nat.card G = 1

Full source

@[to_additive (attr := simp) card_nsmul_eq_zero']
theorem pow_card_eq_one' {G : Type*} [Group G] {x : G} : x ^ Nat.card G = 1 :=
  orderOf_dvd_iff_pow_eq_one.mp <| orderOf_dvd_natCard _

Element Raised to Group Cardinality is Identity

Informal description

For any element $x$ in a group $G$, raising $x$ to the power of the cardinality of $G$ (as a type) yields the identity element, i.e., $x^{|G|} = 1$.

pow_card_eq_one theorem

: x ^ Fintype.card G = 1

Full source

@[to_additive (attr := simp) card_nsmul_eq_zero]
theorem pow_card_eq_one : x ^ Fintype.card G = 1 := by
  rw [← Nat.card_eq_fintype_card, pow_card_eq_one']

Lagrange's Theorem for Finite Groups: $x^{|G|} = 1$

Informal description

For any element $x$ in a finite group $G$, raising $x$ to the power of the cardinality of $G$ yields the identity element, i.e., $x^{|G|} = 1$.

Subgroup.pow_index_mem theorem

{G : Type*} [Group G] (H : Subgroup G) [Normal H] (g : G) : g ^ index H ∈ H

Full source

@[to_additive]
theorem Subgroup.pow_index_mem {G : Type*} [Group G] (H : Subgroup G) [Normal H] (g : G) :
    g ^ index H ∈ H := by rw [← eq_one_iff, QuotientGroup.mk_pow H, index, pow_card_eq_one']

Element Raised to Index Power Belongs to Normal Subgroup

Informal description

For any normal subgroup $H$ of a group $G$ and any element $g \in G$, the element $g$ raised to the power of the index of $H$ in $G$ belongs to $H$, i.e., $g^{[G:H]} \in H$.

pow_mod_card theorem

(a : G) (n : ℕ) : a ^ (n % card G) = a ^ n

Full source

@[to_additive (attr := simp) mod_card_nsmul]
lemma pow_mod_card (a : G) (n : ℕ) : a ^ (n % card G) = a ^ n := by
  rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n orderOf_dvd_card, pow_mod_orderOf]

Exponent Reduction Modulo Group Order: $a^{n \bmod |G|} = a^n$

Informal description

For any element $a$ in a finite group $G$ and any natural number $n$, we have $a^{n \bmod |G|} = a^n$, where $|G|$ denotes the cardinality of $G$.

zpow_mod_card theorem

(a : G) (n : ℤ) : a ^ (n % Fintype.card G : ℤ) = a ^ n

Full source

@[to_additive (attr := simp) mod_card_zsmul]
theorem zpow_mod_card (a : G) (n : ℤ) : a ^ (n % Fintype.card G : ℤ) = a ^ n := by
  rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n
    (Int.natCast_dvd_natCast.2 orderOf_dvd_card), zpow_mod_orderOf]

Exponent Reduction Modulo Group Order: $a^{n \bmod |G|} = a^n$

Informal description

For any element $a$ in a finite group $G$ and any integer $n$, we have $a^{n \bmod |G|} = a^n$, where $|G|$ denotes the cardinality of $G$.

pow_mod_natCard theorem

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

Full source

@[to_additive (attr := simp) mod_natCard_nsmul]
lemma pow_mod_natCard {G} [Group G] (a : G) (n : ℕ) : a ^ (n % Nat.card G) = a ^ n := by
  rw [eq_comm, ← pow_mod_orderOf, ← Nat.mod_mod_of_dvd n <| orderOf_dvd_natCard _, pow_mod_orderOf]

Exponent Reduction Modulo Group Cardinality: $a^{n \bmod |G|} = a^n$

Informal description

For any element $a$ in a group $G$ and any natural number $n$, we have $a^{n \bmod |G|} = a^n$, where $|G|$ denotes the cardinality of $G$ as a type.

zpow_mod_natCard theorem

{G} [Group G] (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n

Full source

@[to_additive (attr := simp) mod_natCard_zsmul]
lemma zpow_mod_natCard {G} [Group G] (a : G) (n : ℤ) : a ^ (n % Nat.card G : ℤ) = a ^ n := by
  rw [eq_comm, ← zpow_mod_orderOf, ← Int.emod_emod_of_dvd n <|
    Int.natCast_dvd_natCast.2 <| orderOf_dvd_natCard _, zpow_mod_orderOf]

Exponent Reduction Modulo Group Cardinality: $a^{n \bmod |G|} = a^n$

Informal description

For any element $a$ in a group $G$ and any integer $n$, we have $a^{n \bmod |G|} = a^n$, where $|G|$ denotes the cardinality of $G$ as a type.

powCoprime definition

{G : Type*} [Group G] (h : (Nat.card G).Coprime n) : G ≃ G

Full source

/-- If `gcd(|G|,n)=1` then the `n`th power map is a bijection -/
@[to_additive (attr := simps) "If `gcd(|G|,n)=1` then the smul by `n` is a bijection"]
noncomputable def powCoprime {G : Type*} [Group G] (h : (Nat.card G).Coprime n) : G ≃ G where
  toFun g := g ^ n
  invFun g := g ^ (Nat.card G).gcdB n
  left_inv g := by
    have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
    dsimp only at key
    rwa [zpow_add, zpow_mul, zpow_mul, zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key
  right_inv g := by
    have key := congr_arg (g ^ ·) ((Nat.card G).gcd_eq_gcd_ab n)
    dsimp only at key
    rwa [zpow_add, zpow_mul, zpow_mul', zpow_natCast, zpow_natCast, zpow_natCast, h.gcd_eq_one,
      pow_one, pow_card_eq_one', one_zpow, one_mul, eq_comm] at key

Power map bijection for coprime exponent

Informal description

Given a finite group $G$ and an integer $n$ coprime to the order of $G$, the function mapping each element $g \in G$ to $g^n$ is a bijection from $G$ to itself. The inverse function maps $g$ to $g^b$, where $b$ is the coefficient from Bézout's identity for $\gcd(|G|, n)$.

powCoprime_one theorem

{G : Type*} [Group G] (h : (Nat.card G).Coprime n) : powCoprime h 1 = 1

Full source

@[to_additive]
theorem powCoprime_one {G : Type*} [Group G] (h : (Nat.card G).Coprime n) : powCoprime h 1 = 1 :=
  one_pow n

Identity Preservation under Power Bijection for Coprime Exponent

Informal description

For any finite group $G$ and integer $n$ coprime to the order of $G$, the bijection $\text{powCoprime}\, h$ maps the identity element $1 \in G$ to itself, i.e., $\text{powCoprime}\, h\, 1 = 1$.

powCoprime_inv theorem

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

Full source

@[to_additive]
theorem powCoprime_inv {G : Type*} [Group G] (h : (Nat.card G).Coprime n) {g : G} :
    powCoprime h g⁻¹ = (powCoprime h g)⁻¹ :=
  inv_pow g n

Inverse Preservation under Power Bijection for Coprime Exponent

Informal description

Let $G$ be a finite group and $n$ an integer coprime to the order of $G$. For any element $g \in G$, the image of the inverse $g^{-1}$ under the bijection $\text{powCoprime}\, h$ is equal to the inverse of the image of $g$, i.e., $\text{powCoprime}\, h\, (g^{-1}) = (\text{powCoprime}\, h\, g)^{-1}$.

Nat.Coprime.pow_left_bijective theorem

{G} [Group G] (hn : (Nat.card G).Coprime n) : Bijective (· ^ n : G → G)

Full source

@[to_additive Nat.Coprime.nsmul_right_bijective]
lemma Nat.Coprime.pow_left_bijective {G} [Group G] (hn : (Nat.card G).Coprime n) :
    Bijective (· ^ n : G → G) :=
  (powCoprime hn).bijective

Bijectivity of Power Map for Coprime Exponent in Finite Groups

Informal description

Let $G$ be a finite group and $n$ an integer coprime to the order of $G$. Then the power map $g \mapsto g^n$ is bijective on $G$.

image_range_orderOf theorem

 [DecidableEq G] :
  letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
  Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (zpowers x : Set G).toFinset

Full source

@[to_additive]
theorem image_range_orderOf [DecidableEq G] :
    letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
    Finset.image (fun i => x ^ i) (Finset.range (orderOf x)) = (zpowers x : Set G).toFinset := by
  letI : Fintype (zpowers x) := (Subgroup.zpowers x).instFintypeSubtypeMemOfDecidablePred
  ext x
  rw [Set.mem_toFinset, SetLike.mem_coe, mem_zpowers_iff_mem_range_orderOf]

Image of Power Map on Order Range Equals Cyclic Subgroup

Informal description

Let $G$ be a monoid with decidable equality and let $x \in G$ be an element of finite order. The image of the finite set $\{0, \ldots, \text{orderOf}(x) - 1\}$ under the power map $i \mapsto x^i$ is equal to the underlying finite set of the cyclic subgroup generated by $x$.

pow_gcd_card_eq_one_iff theorem

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

Full source

@[to_additive gcd_nsmul_card_eq_zero_iff]
theorem pow_gcd_card_eq_one_iff : x ^ n = 1 ↔ x ^ gcd n (Fintype.card G) = 1 :=
  ⟨fun h => pow_gcd_eq_one _ h <| pow_card_eq_one, fun h => by
    let ⟨m, hm⟩ := gcd_dvd_left n (Fintype.card G)
    rw [hm, pow_mul, h, one_pow]⟩

Equivalence of Power Identity and GCD Power Identity in Finite Groups: $x^n = 1 \leftrightarrow x^{\gcd(n, |G|)} = 1$

Informal description

For an element $x$ in a finite group $G$ and a natural number $n$, the equation $x^n = 1$ holds if and only if $x^{\gcd(n, |G|)} = 1$, where $|G|$ is the order of the group $G$.

smul_eq_of_le_smul theorem

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

Full source

lemma smul_eq_of_le_smul
    {G : Type*} [Group G] [Finite G] {α : Type*} [PartialOrder α] {g : G} {a : α}
    [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : a ≤ g • a) : g • a = a := by
  have key := smul_mono_right g (le_pow_smul h (Nat.card G - 1))
  rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
  exact le_antisymm key h

Fixed Point Property for Order-Preserving Group Actions

Informal description

Let $G$ be a finite group acting on a partially ordered set $\alpha$ via scalar multiplication, where the action is order-preserving (i.e., $a \leq b$ implies $g \cdot a \leq g \cdot b$ for all $g \in G$). If for some $g \in G$ and $a \in \alpha$ we have $a \leq g \cdot a$, then $g \cdot a = a$.

smul_eq_of_smul_le theorem

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

Full source

lemma smul_eq_of_smul_le
    {G : Type*} [Group G] [Finite G] {α : Type*} [PartialOrder α] {g : G} {a : α}
    [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le] (h : g • a ≤ a) : g • a = a := by
  have key := smul_mono_right g (pow_smul_le h (Nat.card G - 1))
  rw [smul_smul, ← _root_.pow_succ',
    Nat.sub_one_add_one_eq_of_pos Nat.card_pos, pow_card_eq_one', one_smul] at key
  exact le_antisymm h key

Fixed Point Property for Order-Preserving Group Actions

Informal description

Let $G$ be a finite group acting on a partially ordered set $\alpha$ such that the action is order-preserving (i.e., $g \bullet a \leq g \bullet b$ whenever $a \leq b$). For any $g \in G$ and $a \in \alpha$, if $g \bullet a \leq a$, then $g \bullet a = a$.

submonoidOfIdempotent definition

{M : Type*} [LeftCancelMonoid M] [Finite M] (S : Set M) (hS1 : S.Nonempty) (hS2 : S * S = S) : Submonoid M

Full source

/-- A nonempty idempotent subset of a finite cancellative monoid is a submonoid -/
@[to_additive "A nonempty idempotent subset of a finite cancellative add monoid is a submonoid"]
def submonoidOfIdempotent {M : Type*} [LeftCancelMonoid M] [Finite M] (S : Set M)
    (hS1 : S.Nonempty) (hS2 : S * S = S) : Submonoid M :=
  have pow_mem (a : M) (ha : a ∈ S) (n : ℕ) : a ^ (n + 1) ∈ S := by
    induction n with
    | zero => rwa [zero_add, pow_one]
    | succ n ih =>
      rw [← hS2, pow_succ]
      exact Set.mul_mem_mul ih ha
  { carrier := S
    one_mem' := by
      obtain ⟨a, ha⟩ := hS1
      rw [← pow_orderOf_eq_one a, ← tsub_add_cancel_of_le (succ_le_of_lt (orderOf_pos a))]
      exact pow_mem a ha (orderOf a - 1)
    mul_mem' := fun ha hb => (congr_arg₂ (· ∈ ·) rfl hS2).mp (Set.mul_mem_mul ha hb) }

Submonoid of an idempotent subset in a finite cancellative monoid

Informal description

Given a finite left cancellative monoid $M$ and a nonempty subset $S \subseteq M$ that is idempotent (i.e., $S \cdot S = S$), the subset $S$ forms a submonoid of $M$. More precisely, the submonoid consists of all elements of $S$, where the identity element is obtained by taking an arbitrary element $a \in S$ and raising it to the power of its order minus one, and the multiplication operation is inherited from $M$ and preserves membership in $S$ due to the idempotence condition.

subgroupOfIdempotent definition

{G : Type*} [Group G] [Finite G] (S : Set G) (hS1 : S.Nonempty) (hS2 : S * S = S) : Subgroup G

Full source

/-- A nonempty idempotent subset of a finite group is a subgroup -/
@[to_additive "A nonempty idempotent subset of a finite add group is a subgroup"]
def subgroupOfIdempotent {G : Type*} [Group G] [Finite G] (S : Set G) (hS1 : S.Nonempty)
    (hS2 : S * S = S) : Subgroup G :=
  { submonoidOfIdempotent S hS1 hS2 with
    carrier := S
    inv_mem' := fun {a} ha => show a⁻¹a⁻¹ ∈ submonoidOfIdempotent S hS1 hS2 by
      rw [← one_mul a⁻¹, ← pow_one a, ← pow_orderOf_eq_one a, ← pow_sub a (orderOf_pos a)]
      exact pow_mem ha (orderOf a - 1) }

Subgroup of an idempotent subset in a finite group

Informal description

Given a finite group $G$ and a nonempty subset $S \subseteq G$ that is idempotent (i.e., $S \cdot S = S$), the subset $S$ forms a subgroup of $G$. The subgroup structure is inherited from the underlying group $G$, with the additional property that for any element $a \in S$, its inverse $a^{-1}$ is also in $S$. This is shown by expressing $a^{-1}$ as a power of $a$ using the order of $a$ in $G$.

powCardSubgroup definition

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

Full source

/-- If `S` is a nonempty subset of a finite group `G`, then `S ^ |G|` is a subgroup -/
@[to_additive (attr := simps!) smulCardAddSubgroup
  "If `S` is a nonempty subset of a finite add group `G`, then `|G| • S` is a subgroup"]
def powCardSubgroup {G : Type*} [Group G] [Fintype G] (S : Set G) (hS : S.Nonempty) : Subgroup G :=
  have one_mem : (1 : G) ∈ S ^ Fintype.card G := by
    obtain ⟨a, ha⟩ := hS
    rw [← pow_card_eq_one]
    exact Set.pow_mem_pow ha
  subgroupOfIdempotent (S ^ Fintype.card G) ⟨1, one_mem⟩ <| by
    classical
    apply (Set.eq_of_subset_of_card_le (Set.subset_mul_left _ one_mem) (ge_of_eq _)).symm
    simp_rw [← pow_add,
        Group.card_pow_eq_card_pow_card_univ S (Fintype.card G + Fintype.card G) le_add_self]

Subgroup generated by $S^{|G|}$ in a finite group

Informal description

Given a finite group $G$ and a nonempty subset $S \subseteq G$, the subset $S^{|G|}$ (the $|G|$-th power of $S$) forms a subgroup of $G$. Here $|G|$ denotes the order of the group $G$.

orderOf_abs_ne_one theorem

(h : |x| ≠ 1) : orderOf x = 0

Full source

theorem orderOf_abs_ne_one (h : |x||x| ≠ 1) : orderOf x = 0 := by
  rw [orderOf_eq_zero_iff']
  intro n hn hx
  replace hx : |x| ^ n = 1 := by simpa only [abs_one, abs_pow] using congr_arg abs hx
  rcases h.lt_or_lt with h | h
  · exact ((pow_lt_one₀ (abs_nonneg x) h hn.ne').ne hx).elim
  · exact ((one_lt_pow₀ h hn.ne').ne' hx).elim

Order of Element with Absolute Value Not Equal to One is Zero

Informal description

For any element $x$ in a monoid $G$, if the absolute value of $x$ is not equal to $1$, then the order of $x$ is zero, i.e., $\text{orderOf}(x) = 0$.

LinearOrderedRing.orderOf_le_two theorem

: orderOf x ≤ 2

Full source

theorem LinearOrderedRing.orderOf_le_two : orderOf x ≤ 2 := by
  rcases ne_or_eq |x| 1 with h | h
  · simp [orderOf_abs_ne_one h]
  rcases eq_or_eq_neg_of_abs_eq h with (rfl | rfl)
  · simp
  exact orderOf_le_of_pow_eq_one zero_lt_two (by simp)

Order Bound in Linearly Ordered Rings: $\text{orderOf}(x) \leq 2$

Informal description

For any element $x$ in a linearly ordered ring, the order of $x$ is at most 2, i.e., $\text{orderOf}(x) \leq 2$.

Prod.orderOf theorem

(x : α × β) : orderOf x = (orderOf x.1).lcm (orderOf x.2)

Full source

@[to_additive]
protected theorem Prod.orderOf (x : α × β) : orderOf x = (orderOf x.1).lcm (orderOf x.2) :=
  minimalPeriod_prodMap _ _ _

Order of Product Element as LCM of Component Orders

Informal description

For any element $x = (x_1, x_2)$ in the direct product of monoids $\alpha \times \beta$, the order of $x$ is equal to the least common multiple of the orders of $x_1$ in $\alpha$ and $x_2$ in $\beta$, i.e., $$\text{orderOf}(x) = \text{lcm}(\text{orderOf}(x_1), \text{orderOf}(x_2)).$$

orderOf_fst_dvd_orderOf theorem

: orderOf x.1 ∣ orderOf x

Full source

@[to_additive]
theorem orderOf_fst_dvd_orderOf : orderOforderOf x.1 ∣ orderOf x :=
  minimalPeriod_fst_dvd

Order of First Component Divides Order of Product Element

Informal description

For any element $x$ in the product monoid $\alpha \times \beta$, the order of the first component $x.1$ divides the order of $x$.

orderOf_snd_dvd_orderOf theorem

: orderOf x.2 ∣ orderOf x

Full source

@[to_additive]
theorem orderOf_snd_dvd_orderOf : orderOforderOf x.2 ∣ orderOf x :=
  minimalPeriod_snd_dvd

Order of Second Component Divides Order in Direct Product

Informal description

For any element $x = (x_1, x_2)$ in the direct product of two monoids, the order of the second component $x_2$ divides the order of $x$.

IsOfFinOrder.fst theorem

{x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.1

Full source

@[to_additive]
theorem IsOfFinOrder.fst {x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.1 :=
  hx.mono orderOf_fst_dvd_orderOf

Finite Order of First Component in Direct Product

Informal description

For any element $x = (x_1, x_2)$ in the direct product of monoids $\alpha \times \beta$, if $x$ has finite order, then the first component $x_1$ also has finite order.

IsOfFinOrder.snd theorem

{x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.2

Full source

@[to_additive]
theorem IsOfFinOrder.snd {x : α × β} (hx : IsOfFinOrder x) : IsOfFinOrder x.2 :=
  hx.mono orderOf_snd_dvd_orderOf

Finite Order of Second Component in Product Monoid

Informal description

For any element $x = (x_1, x_2)$ in the direct product of monoids $\alpha \times \beta$, if $x$ has finite order, then the second component $x_2$ also has finite order.

IsOfFinOrder.prod_mk theorem

: IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b)

Full source

@[to_additive IsOfFinAddOrder.prod_mk]
theorem IsOfFinOrder.prod_mk : IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b) := by
  simpa only [← orderOf_pos_iff, Prod.orderOf] using Nat.lcm_pos

Finite Order of Product Elements

Informal description

For elements $a$ in a monoid $\alpha$ and $b$ in a monoid $\beta$, if $a$ and $b$ are of finite order, then the pair $(a, b)$ in the product monoid $\alpha \times \beta$ is also of finite order.

Prod.orderOf_mk theorem

: orderOf (a, b) = Nat.lcm (orderOf a) (orderOf b)

Full source

@[to_additive]
lemma Prod.orderOf_mk : orderOf (a, b) = Nat.lcm (orderOf a) (orderOf b) :=
  (a, b).orderOf

Order of Product Element as LCM of Component Orders

Informal description

For any elements $a$ in a monoid $\alpha$ and $b$ in a monoid $\beta$, the order of the pair $(a, b)$ in the product monoid $\alpha \times \beta$ is equal to the least common multiple of the orders of $a$ and $b$, i.e., $$\text{orderOf}(a, b) = \text{lcm}(\text{orderOf}(a), \text{orderOf}(b)).$$

Nat.cast_card_eq_zero theorem

(R) [AddGroupWithOne R] [Fintype R] : (Fintype.card R : R) = 0

Full source

@[simp]
lemma Nat.cast_card_eq_zero (R) [AddGroupWithOne R] [Fintype R] : (Fintype.card R : R) = 0 := by
  rw [← nsmul_one, card_nsmul_eq_zero]

Cardinality Cast to Zero in Finite Additive Group with One

Informal description

For any additive group with one $(R, +, 0, 1)$ and any finite type $R$, the canonical image of the cardinality of $R$ in $R$ itself is equal to zero, i.e., $(\text{card}(R) : R) = 0$.

CharP.addOrderOf_one theorem

: CharP R (addOrderOf (1 : R))

Full source

lemma CharP.addOrderOf_one : CharP R (addOrderOf (1 : R)) where
  cast_eq_zero_iff n := by rw [← Nat.smul_one_eq_cast, addOrderOf_dvd_iff_nsmul_eq_zero]

Characteristic as Additive Order of Unity

Informal description

For any additive group with one $(R, +, 0, 1)$, the characteristic of $R$ is equal to the additive order of the element $1 \in R$, i.e., $\text{CharP}(R) = \text{addOrderOf}(1)$.

charP_of_ne_zero theorem

(hn : card R = p) (hR : ∀ i < p, (i : R) = 0 → i = 0) : CharP R p

Full source

lemma charP_of_ne_zero (hn : card R = p) (hR : ∀ i < p, (i : R) = 0 → i = 0) : CharP R p where
  cast_eq_zero_iff n := by
    have H : (p : R) = 0 := by rw [← hn, Nat.cast_card_eq_zero]
    constructor
    · intro h
      rw [← Nat.mod_add_div n p, Nat.cast_add, Nat.cast_mul, H, zero_mul, add_zero] at h
      rw [Nat.dvd_iff_mod_eq_zero]
      apply hR _ (Nat.mod_lt _ _) h
      rw [← hn, gt_iff_lt, Fintype.card_pos_iff]
      exact ⟨0⟩
    · rintro ⟨n, rfl⟩
      rw [Nat.cast_mul, H, zero_mul]

Characterization of Ring Characteristic via Cardinality and Injectivity

Informal description

Let $R$ be a finite ring with $\text{card}(R) = p$ for some natural number $p$. If for every natural number $i < p$, the condition $(i : R) = 0$ implies $i = 0$, then $R$ has characteristic $p$.

charP_of_prime_pow_injective theorem

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

Full source

lemma charP_of_prime_pow_injective (R) [Ring R] [Fintype R] (p n : ℕ) [hp : Fact p.Prime]
    (hn : card R = p ^ n) (hR : ∀ i ≤ n, (p : R) ^ i = 0 → i = n) : CharP R (p ^ n) := by
  obtain ⟨c, hc⟩ := CharP.exists R
  have hcpn : c ∣ p ^ n := by rw [← CharP.cast_eq_zero_iff R c, ← hn, Nat.cast_card_eq_zero]
  obtain ⟨i, hi, rfl⟩ : ∃ i ≤ n, c = p ^ i := by rwa [Nat.dvd_prime_pow hp.1] at hcpn
  obtain rfl : i = n := hR i hi <| by rw [← Nat.cast_pow, CharP.cast_eq_zero]
  assumption

Characterization of Ring Characteristic as Prime Power via Injectivity Condition

Informal description

Let $R$ be a finite ring with cardinality $p^n$ where $p$ is a prime number and $n$ is a natural number. If for every natural number $i \leq n$, the condition $(p : R)^i = 0$ implies $i = n$, then the characteristic of $R$ is $p^n$.

SemiconjBy.orderOf_eq theorem

[Group G] (a : G) {x y : G} (h : SemiconjBy a x y) : orderOf x = orderOf y

Full source

@[to_additive]
lemma orderOf_eq [Group G] (a : G) {x y : G} (h : SemiconjBy a x y) : orderOf x = orderOf y := by
  rw [orderOf_eq_orderOf_iff]
  intro n
  exact (h.pow_right n).eq_one_iff

Order Preservation under Semiconjugation in Groups

Informal description

Let $G$ be a group and let $a, x, y \in G$ such that $a$ semiconjugates $x$ to $y$ (i.e., $a x = y a$). Then the order of $x$ equals the order of $y$.

orderOf_piMulSingle theorem

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

Full source

lemma orderOf_piMulSingle {ι : Type*} [DecidableEq ι] {M : ι → Type*} [(i : ι) → Monoid (M i)]
    (i : ι) (g : M i) :
    orderOf (Pi.mulSingle i g) = orderOf g :=
  orderOf_injective (MonoidHom.mulSingle M i) (Pi.mulSingle_injective M i) g

Order Preservation under $\text{mulSingle}$ in Product Monoid

Informal description

Let $\{M_i\}_{i \in \iota}$ be a family of monoids indexed by a decidable type $\iota$, and let $g \in M_i$ for some fixed $i \in \iota$. The order of the element $\text{mulSingle}_i(g)$ in the product monoid $\prod_{i \in \iota} M_i$ (which is $g$ in the $i$-th component and $1$ elsewhere) is equal to the order of $g$ in $M_i$.

Mathlib.GroupTheory.OrderOfElement

Main definitions

Tags