Mathlib.GroupTheory.Exponent

Monoid.ExponentExists definition

Full source

/-- A predicate on a monoid saying that there is a positive integer `n` such that `g ^ n = 1`
  for all `g`. -/
@[to_additive
      "A predicate on an additive monoid saying that there is a positive integer `n` such\n
      that `n • g = 0` for all `g`."]
def ExponentExists :=
  ∃ n, 0 < n ∧ ∀ g : G, g ^ n = 1

Existence of exponent for a monoid

Informal description

A monoid $G$ satisfies the predicate `Monoid.ExponentExists` if there exists a positive integer $n$ such that for every element $g \in G$, $g^n = 1$.

Monoid.exponent definition

Full source

/-- The exponent of a group is the smallest positive integer `n` such that `g ^ n = 1` for all
  `g ∈ G` if it exists, otherwise it is zero by convention. -/
@[to_additive
      "The exponent of an additive group is the smallest positive integer `n` such that\n
      `n • g = 0` for all `g ∈ G` if it exists, otherwise it is zero by convention."]
noncomputable def exponent :=
  if h : ExponentExists G then Nat.find h else 0

Exponent of a monoid

Informal description

The exponent of a monoid $G$ is defined as the smallest positive integer $n$ such that $g^n = 1$ for all $g \in G$, if such an $n$ exists. If no such $n$ exists, the exponent is defined to be $0$.

AddMonoid.exponent_additive theorem

: AddMonoid.exponent (Additive G) = exponent G

Full source

@[simp]
theorem _root_.AddMonoid.exponent_additive :
    AddMonoid.exponent (Additive G) = exponent G := rfl

Exponent Equality Between Additive and Multiplicative Monoids

Informal description

For any monoid $G$, the exponent of the additive monoid $\text{Additive}(G)$ is equal to the exponent of $G$ as a multiplicative monoid.

Monoid.exponent_multiplicative theorem

{G : Type*} [AddMonoid G] : exponent (Multiplicative G) = AddMonoid.exponent G

Full source

@[simp]
theorem exponent_multiplicative {G : Type*} [AddMonoid G] :
    exponent (Multiplicative G) = AddMonoid.exponent G := rfl

Exponent Equality Between Multiplicative and Additive Monoids

Informal description

For any additive monoid $G$, the exponent of the multiplicative monoid $\text{Multiplicative}(G)$ is equal to the exponent of $G$ as an additive monoid.

MulOpposite.exponent theorem

: exponent (MulOpposite G) = exponent G

Full source

@[to_additive (attr := simp)]
theorem _root_.MulOpposite.exponent : exponent (MulOpposite G) = exponent G := by
  simp only [Monoid.exponent, ExponentExists]
  congr!
  all_goals exact ⟨(op_injective <| · <| op ·), (unop_injective <| · <| unop ·)⟩

Exponent Equality Between Monoid and Its Opposite

Informal description

The exponent of the opposite monoid $\text{MulOpposite}(G)$ is equal to the exponent of the original monoid $G$.

Monoid.ExponentExists.isOfFinOrder theorem

(h : ExponentExists G) {g : G} : IsOfFinOrder g

Full source

@[to_additive]
theorem ExponentExists.isOfFinOrder (h : ExponentExists G) {g : G} : IsOfFinOrder g :=
  isOfFinOrder_iff_pow_eq_one.mpr <| by peel 2 h; exact this g

Existence of Exponent Implies All Elements Have Finite Order

Informal description

If a monoid $G$ has an exponent (i.e., there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$), then every element $g \in G$ has finite order.

Monoid.ExponentExists.orderOf_pos theorem

(h : ExponentExists G) (g : G) : 0 < orderOf g

Full source

@[to_additive]
theorem ExponentExists.orderOf_pos (h : ExponentExists G) (g : G) : 0 < orderOf g :=
  h.isOfFinOrder.orderOf_pos

Positivity of Element Orders in Monoids with Exponent

Informal description

If a monoid $G$ has an exponent (i.e., there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$), then for every element $g \in G$, the order of $g$ is positive, i.e., $\text{orderOf}(g) > 0$.

Monoid.exponent_ne_zero theorem

: exponent G ≠ 0 ↔ ExponentExists G

Full source

@[to_additive]
theorem exponent_ne_zero : exponentexponent G ≠ 0exponent G ≠ 0 ↔ ExponentExists G := by
  rw [exponent]
  split_ifs with h
  · simp [h, @not_lt_zero' ℕ]
  --if this isn't done this way, `to_additive` freaks
  · tauto

Nonzero Exponent Criterion for Monoids

Informal description

The exponent of a monoid $G$ is nonzero if and only if there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$.

Monoid.exponent_pos theorem

: 0 < exponent G ↔ ExponentExists G

Full source

@[to_additive]
theorem exponent_pos : 0 < exponent G ↔ ExponentExists G :=
  pos_iff_ne_zero.trans exponent_ne_zero

Positivity of Exponent Criterion for Monoids

Informal description

The exponent of a monoid $G$ is positive if and only if there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$.

Monoid.exponent_eq_zero_iff theorem

: exponent G = 0 ↔ ¬ExponentExists G

Full source

@[to_additive]
theorem exponent_eq_zero_iff : exponentexponent G = 0 ↔ ¬ExponentExists G :=
  exponent_ne_zero.not_right

Exponent Zero Criterion for Monoids

Informal description

The exponent of a monoid $G$ is zero if and only if there does not exist a positive integer $n$ such that $g^n = 1$ for all $g \in G$.

Monoid.exponent_eq_zero_of_order_zero theorem

{g : G} (hg : orderOf g = 0) : exponent G = 0

Full source

@[to_additive exponent_eq_zero_addOrder_zero]
theorem exponent_eq_zero_of_order_zero {g : G} (hg : orderOf g = 0) : exponent G = 0 :=
  exponent_eq_zero_iff.mpr fun h ↦ h.orderOf_pos g |>.ne' hg

Exponent is Zero for Monoids with Elements of Infinite Order

Informal description

For any element $g$ in a monoid $G$, if the order of $g$ is zero (i.e., $g$ has infinite order), then the exponent of $G$ is zero.

Monoid.exponent_eq_zero_iff_forall theorem

: exponent G = 0 ↔ ∀ n > 0, ∃ g : G, g ^ n ≠ 1

Full source

/-- The exponent is zero iff for all nonzero `n`, one can find a `g` such that `g ^ n ≠ 1`. -/
@[to_additive "The exponent is zero iff for all nonzero `n`, one can find a `g` such that
`n • g ≠ 0`."]
theorem exponent_eq_zero_iff_forall : exponentexponent G = 0 ↔ ∀ n > 0, ∃ g : G, g ^ n ≠ 1 := by
  rw [exponent_eq_zero_iff, ExponentExists]
  push_neg
  rfl

Characterization of Zero Exponent: $\text{exp}(G) = 0 \leftrightarrow \forall n>0, \exists g \in G, g^n \neq 1$

Informal description

The exponent of a monoid $G$ is zero if and only if for every positive integer $n$, there exists an element $g \in G$ such that $g^n \neq 1$.

Monoid.pow_exponent_eq_one theorem

(g : G) : g ^ exponent G = 1

Full source

@[to_additive exponent_nsmul_eq_zero]
theorem pow_exponent_eq_one (g : G) : g ^ exponent G = 1 := by
  classical
  by_cases h : ExponentExists G
  · simp_rw [exponent, dif_pos h]
    exact (Nat.find_spec h).2 g
  · simp_rw [exponent, dif_neg h, pow_zero]

Element Raised to Exponent Yields Identity

Informal description

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

Monoid.pow_eq_mod_exponent theorem

{n : ℕ} (g : G) : g ^ n = g ^ (n % exponent G)

Full source

@[to_additive]
theorem pow_eq_mod_exponent {n : ℕ} (g : G) : g ^ n = g ^ (n % exponent G) :=
  calc
    g ^ n = g ^ (n % exponent G + exponent G * (n / exponent G)) := by rw [Nat.mod_add_div]
    _ = g ^ (n % exponent G) := by simp [pow_add, pow_mul, pow_exponent_eq_one]

Exponent Periodicity: $g^n = g^{n \bmod \text{exp}(G)}$

Informal description

For any element $g$ in a monoid $G$ and any natural number $n$, the power $g^n$ is equal to $g^{n \bmod \text{exp}(G)}$, where $\text{exp}(G)$ is the exponent of $G$.

Monoid.exponent_pos_of_exists theorem

(n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) : 0 < exponent G

Full source

@[to_additive]
theorem exponent_pos_of_exists (n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) :
    0 < exponent G :=
  ExponentExists.exponent_pos ⟨n, hpos, hG⟩

Positivity of Exponent When All Elements Have Finite Order

Informal description

For any monoid $G$ and positive integer $n$, if $g^n = 1$ for all $g \in G$, then the exponent of $G$ is positive.

Monoid.exponent_min' theorem

(n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) : exponent G ≤ n

Full source

@[to_additive]
theorem exponent_min' (n : ℕ) (hpos : 0 < n) (hG : ∀ g : G, g ^ n = 1) : exponent G ≤ n := by
  classical
  rw [exponent, dif_pos]
  · apply Nat.find_min'
    exact ⟨hpos, hG⟩
  · exact ⟨n, hpos, hG⟩

Exponent Minimality: $\exp(G) \leq n$ if $g^n = 1$ for all $g \in G$

Informal description

For any monoid $G$ and positive integer $n$, if $g^n = 1$ for all $g \in G$, then the exponent of $G$ is less than or equal to $n$.

Monoid.exponent_min theorem

(m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ g : G, g ^ m ≠ 1

Full source

@[to_additive]
theorem exponent_min (m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ g : G, g ^ m ≠ 1 := by
  by_contra! h
  have hcon : exponent G ≤ m := exponent_min' m hpos h
  omega

Exponent Lower Bound: Existence of Non-Identity Power for $m < \exp(G)$

Informal description

For any monoid $G$ and positive integer $m$, if $m$ is strictly less than the exponent of $G$, then there exists an element $g \in G$ such that $g^m \neq 1$.

Monoid.exp_eq_one_iff theorem

: exponent G = 1 ↔ Subsingleton G

Full source

@[to_additive AddMonoid.exp_eq_one_iff]
theorem exp_eq_one_iff : exponentexponent G = 1 ↔ Subsingleton G := by
  refine ⟨fun eq_one => ⟨fun a b => ?a_eq_b⟩, fun h => le_antisymm ?le ?ge⟩
  · rw [← pow_one a, ← pow_one b, ← eq_one, Monoid.pow_exponent_eq_one, Monoid.pow_exponent_eq_one]
  · apply exponent_min' _ Nat.one_pos
    simp [eq_iff_true_of_subsingleton]
  · apply Nat.succ_le_of_lt
    apply exponent_pos_of_exists 1 Nat.one_pos
    simp [eq_iff_true_of_subsingleton]

Exponent One if and only if Monoid is Subsingleton

Informal description

The exponent of a monoid $G$ is equal to $1$ if and only if $G$ is a subsingleton (i.e., all elements of $G$ are equal).

Monoid.exp_eq_one_of_subsingleton theorem

[hs : Subsingleton G] : exponent G = 1

Full source

@[to_additive (attr := simp) AddMonoid.exp_eq_one_of_subsingleton]
theorem exp_eq_one_of_subsingleton [hs : Subsingleton G] : exponent G = 1 :=
  exp_eq_one_iff.mpr hs

Exponent of a Subsingleton Monoid is One

Informal description

For any subsingleton monoid $G$ (i.e., a monoid with at most one element), the exponent of $G$ is equal to $1$.

Monoid.order_dvd_exponent theorem

(g : G) : orderOf g ∣ exponent G

Full source

@[to_additive addOrder_dvd_exponent]
theorem order_dvd_exponent (g : G) : orderOforderOf g ∣ exponent G :=
  orderOf_dvd_of_pow_eq_one <| pow_exponent_eq_one g

Order Divides Exponent in Monoids

Informal description

For any element $g$ in a monoid $G$, the order of $g$ divides the exponent of $G$, i.e., $\text{orderOf}(g) \mid \text{exponent}(G)$.

Monoid.orderOf_le_exponent theorem

(h : ExponentExists G) (g : G) : orderOf g ≤ exponent G

Full source

@[to_additive]
theorem orderOf_le_exponent (h : ExponentExists G) (g : G) : orderOf g ≤ exponent G :=
  Nat.le_of_dvd h.exponent_pos (order_dvd_exponent g)

Order of Element Bounded by Exponent in Monoids

Informal description

For any monoid $G$ with an exponent (i.e., there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$), the order of any element $g \in G$ is less than or equal to the exponent of $G$. In other words, $\text{orderOf}(g) \leq \text{exponent}(G)$.

Monoid.exponent_dvd_iff_forall_pow_eq_one theorem

{n : ℕ} : exponent G ∣ n ↔ ∀ g : G, g ^ n = 1

Full source

@[to_additive]
theorem exponent_dvd_iff_forall_pow_eq_one {n : ℕ} : exponentexponent G ∣ nexponent G ∣ n ↔ ∀ g : G, g ^ n = 1 := by
  rcases n.eq_zero_or_pos with (rfl | hpos)
  · simp
  constructor
  · intro h g
    rw [Nat.dvd_iff_mod_eq_zero] at h
    rw [pow_eq_mod_exponent, h, pow_zero]
  · intro hG
    by_contra h
    rw [Nat.dvd_iff_mod_eq_zero, ← Ne, ← pos_iff_ne_zero] at h
    have h₂ : n % exponent G < exponent G := Nat.mod_lt _ (exponent_pos_of_exists n hpos hG)
    have h₃ : exponent G ≤ n % exponent G := by
      apply exponent_min' _ h
      simp_rw [← pow_eq_mod_exponent]
      exact hG
    exact h₂.not_le h₃

Exponent Divisibility Criterion: $\text{exp}(G) \mid n \leftrightarrow \forall g \in G, g^n = 1$

Informal description

For a monoid $G$ and a natural number $n$, the exponent of $G$ divides $n$ if and only if $g^n = 1$ for all $g \in G$.

Monoid.exponent_dvd theorem

{n : ℕ} : exponent G ∣ n ↔ ∀ g : G, orderOf g ∣ n

Full source

@[to_additive]
theorem exponent_dvd {n : ℕ} : exponentexponent G ∣ nexponent G ∣ n ↔ ∀ g : G, orderOf g ∣ n := by
  simp_rw [exponent_dvd_iff_forall_pow_eq_one, orderOf_dvd_iff_pow_eq_one]

Exponent Divides $n$ if and only if All Element Orders Divide $n$

Informal description

For a monoid $G$ and a natural number $n$, the exponent of $G$ divides $n$ if and only if the order of every element $g \in G$ divides $n$.

Monoid.lcm_orderOf_dvd_exponent theorem

[Fintype G] : (Finset.univ : Finset G).lcm orderOf ∣ exponent G

Full source

@[to_additive]
theorem lcm_orderOf_dvd_exponent [Fintype G] :
    (Finset.univ : Finset G).lcm orderOf ∣ exponent G := by
  apply Finset.lcm_dvd
  intro g _
  exact order_dvd_exponent g

Least Common Multiple of Element Orders Divides Exponent in Finite Monoids

Informal description

For a finite monoid $G$, the least common multiple of the orders of all elements in $G$ divides the exponent of $G$. In other words, $\text{lcm}\{\text{orderOf}(g) \mid g \in G\} \mid \text{exponent}(G)$.

Nat.Prime.exists_orderOf_eq_pow_factorization_exponent theorem

{p : ℕ} (hp : p.Prime) : ∃ g : G, orderOf g = p ^ (exponent G).factorization p

Full source

@[to_additive exists_addOrderOf_eq_pow_padic_val_nat_add_exponent]
theorem _root_.Nat.Prime.exists_orderOf_eq_pow_factorization_exponent {p : ℕ} (hp : p.Prime) :
    ∃ g : G, orderOf g = p ^ (exponent G).factorization p := by
  haveI := Fact.mk hp
  rcases eq_or_ne ((exponent G).factorization p) 0 with (h | h)
  · refine ⟨1, by rw [h, pow_zero, orderOf_one]⟩
  have he : 0 < exponent G :=
    Ne.bot_lt fun ht => by
      rw [ht] at h
      apply h
      rw [bot_eq_zero, Nat.factorization_zero, Finsupp.zero_apply]
  rw [← Finsupp.mem_support_iff] at h
  obtain ⟨g, hg⟩ : ∃ g : G, g ^ (exponent G / p) ≠ 1 := by
    suffices key : ¬exponent G ∣ exponent G / p by
      rwa [exponent_dvd_iff_forall_pow_eq_one, not_forall] at key
    exact fun hd =>
      hp.one_lt.not_le
        ((mul_le_iff_le_one_left he).mp <|
          Nat.le_of_dvd he <| Nat.mul_dvd_of_dvd_div (Nat.dvd_of_mem_primeFactors h) hd)
  obtain ⟨k, hk : exponent G = p ^ _ * k⟩ := Nat.ordProj_dvd _ _
  obtain ⟨t, ht⟩ := Nat.exists_eq_succ_of_ne_zero (Finsupp.mem_support_iff.mp h)
  refine ⟨g ^ k, ?_⟩
  rw [ht]
  apply orderOf_eq_prime_pow
  · rwa [hk, mul_comm, ht, pow_succ, ← mul_assoc, Nat.mul_div_cancel _ hp.pos, pow_mul] at hg
  · rw [← Nat.succ_eq_add_one, ← ht, ← pow_mul, mul_comm, ← hk]
    exact pow_exponent_eq_one g

Existence of Element with Order as Prime Power in Exponent's Factorization

Informal description

For any prime number $p$ and any monoid $G$, there exists an element $g \in G$ whose order is equal to $p$ raised to the power of the exponent of $G$'s prime factorization at $p$, i.e., $\text{orderOf}(g) = p^{(\text{exponent}(G)).\text{factorization}(p)}$.

Commute.orderOf_mul_pow_eq_lcm theorem

 {x y : G} (h : Commute x y) (hx : orderOf x ≠ 0) (hy : orderOf y ≠ 0) :
  orderOf
      (x ^ (orderOf x / (factorizationLCMLeft (orderOf x) (orderOf y))) *
        y ^ (orderOf y / factorizationLCMRight (orderOf x) (orderOf y))) =
    Nat.lcm (orderOf x) (orderOf y)

Full source

/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element
of order `lcm n m`. The result actually gives an explicit (computable) element, written as the
product of a power of `x` and a power of `y`. See also the result below if you don't need the
explicit formula. -/
@[to_additive "If two commuting elements `x` and `y` of an additive monoid have order `n` and `m`,
there is an element of order `lcm n m`. The result actually gives an explicit (computable) element,
written as the sum of a multiple of `x` and a multiple of `y`. See also the result below if you
don't need the explicit formula."]
lemma _root_.Commute.orderOf_mul_pow_eq_lcm {x y : G} (h : Commute x y) (hx : orderOforderOf x ≠ 0)
    (hy : orderOforderOf y ≠ 0) :
    orderOf (x ^ (orderOf x / (factorizationLCMLeft (orderOf x) (orderOf y))) *
      y ^ (orderOf y / factorizationLCMRight (orderOf x) (orderOf y))) =
      Nat.lcm (orderOf x) (orderOf y) := by
  rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
  all_goals iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
  all_goals simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
    factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]

Order of Product of Powers of Commuting Elements Equals LCM of Orders

Informal description

Let $x$ and $y$ be commuting elements in a monoid $G$ with finite orders $\text{orderOf}(x) \neq 0$ and $\text{orderOf}(y) \neq 0$. Then the order of the element $x^{a} \cdot y^{b}$, where $a = \text{orderOf}(x)/d_1$ and $b = \text{orderOf}(y)/d_2$ (with $d_1$ and $d_2$ being the left and right factorization components of the least common multiple), is equal to the least common multiple of $\text{orderOf}(x)$ and $\text{orderOf}(y)$, i.e., $$\text{orderOf}\big(x^{a} \cdot y^{b}\big) = \text{lcm}(\text{orderOf}(x), \text{orderOf}(y)).$$

Commute.exists_orderOf_eq_lcm theorem

{x y : G} (h : Commute x y) : ∃ z ∈ closure { x, y }, orderOf z = Nat.lcm (orderOf x) (orderOf y)

Full source

/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, then there is an
element of order `lcm n m` that lies in the subgroup generated by `x` and `y`. -/
@[to_additive "If two commuting elements `x` and `y` of an additive monoid have order `n` and `m`,
then there is an element of order `lcm n m` that lies in the additive subgroup generated by `x`
and `y`."]
theorem _root_.Commute.exists_orderOf_eq_lcm {x y : G} (h : Commute x y) :
    ∃ z ∈ closure {x, y}, orderOf z = Nat.lcm (orderOf x) (orderOf y) := by
  by_cases hx : orderOf x = 0 <;> by_cases hy : orderOf y = 0
  · exact ⟨x, subset_closure (by simp), by simp [hx]⟩
  · exact ⟨x, subset_closure (by simp), by simp [hx]⟩
  · exact ⟨y, subset_closure (by simp), by simp [hy]⟩
  · exact ⟨_, mul_mem (pow_mem (subset_closure (by simp)) _) (pow_mem (subset_closure (by simp)) _),
      h.orderOf_mul_pow_eq_lcm hx hy⟩

Existence of Element with Order LCM in Generated Subgroup

Informal description

Let $x$ and $y$ be commuting elements in a monoid $G$. Then there exists an element $z$ in the subgroup generated by $x$ and $y$ such that the order of $z$ is equal to the least common multiple of the orders of $x$ and $y$, i.e., $$\text{orderOf}(z) = \text{lcm}(\text{orderOf}(x), \text{orderOf}(y)).$$

Monoid.exponent_eq_prime_iff theorem

 {G : Type*} [Monoid G] [Nontrivial G] {p : ℕ} (hp : p.Prime) : Monoid.exponent G = p ↔ ∀ g : G, g ≠ 1 → orderOf g = p

Full source

/-- A nontrivial monoid has prime exponent `p` if and only if every non-identity element has
order `p`. -/
@[to_additive]
lemma exponent_eq_prime_iff {G : Type*} [Monoid G] [Nontrivial G] {p : ℕ} (hp : p.Prime) :
    Monoid.exponentMonoid.exponent G = p ↔ ∀ g : G, g ≠ 1 → orderOf g = p := by
  refine ⟨fun hG g hg ↦ ?_, fun h ↦ dvd_antisymm ?_ ?_⟩
  · rw [Ne, ← orderOf_eq_one_iff] at hg
    exact Eq.symm <| (hp.dvd_iff_eq hg).mp <| hG ▸ Monoid.order_dvd_exponent g
  · rw [exponent_dvd]
    intro g
    by_cases hg : g = 1
    · simp [hg]
    · rw [h g hg]
  · obtain ⟨g, hg⟩ := exists_ne (1 : G)
    simpa [h g hg] using Monoid.order_dvd_exponent g

Characterization of Monoids with Prime Exponent: $\text{exponent}(G) = p \leftrightarrow \forall g \neq 1, \text{orderOf}(g) = p$

Informal description

Let $G$ be a nontrivial monoid and $p$ a prime number. The exponent of $G$ is equal to $p$ if and only if every non-identity element $g \in G$ has order $p$, i.e., $$\text{exponent}(G) = p \leftrightarrow \forall g \in G, g \neq 1 \rightarrow \text{orderOf}(g) = p.$$

Monoid.exponent_ne_zero_iff_range_orderOf_finite theorem

(h : ∀ g : G, 0 < orderOf g) : exponent G ≠ 0 ↔ (Set.range (orderOf : G → ℕ)).Finite

Full source

@[to_additive]
theorem exponent_ne_zero_iff_range_orderOf_finite (h : ∀ g : G, 0 < orderOf g) :
    exponentexponent G ≠ 0exponent G ≠ 0 ↔ (Set.range (orderOf : G → ℕ)).Finite := by
  refine ⟨fun he => ?_, fun he => ?_⟩
  · by_contra h
    obtain ⟨m, ⟨t, rfl⟩, het⟩ := Set.Infinite.exists_gt h (exponent G)
    exact pow_ne_one_of_lt_orderOf he het (pow_exponent_eq_one t)
  · lift Set.range (orderOf (G := G)) to Finset ℕ using he with t ht
    have htpos : 0 < t.prod id := by
      refine Finset.prod_pos fun a ha => ?_
      rw [← Finset.mem_coe, ht] at ha
      obtain ⟨k, rfl⟩ := ha
      exact h k
    suffices exponentexponent G ∣ t.prod id by
      intro h
      rw [h, zero_dvd_iff] at this
      exact htpos.ne' this
    rw [exponent_dvd]
    intro g
    apply Finset.dvd_prod_of_mem id (?_ : orderOforderOf g ∈ _)
    rw [← Finset.mem_coe, ht]
    exact Set.mem_range_self g

Nonzero Exponent Characterization via Finite Order Range

Informal description

For a monoid $G$ where every element has positive order, the exponent of $G$ is nonzero if and only if the set of orders of all elements in $G$ is finite. That is, $\text{exponent}(G) \neq 0 \leftrightarrow \{\text{orderOf}(g) \mid g \in G\}$ is finite.

Monoid.exponent_eq_zero_iff_range_orderOf_infinite theorem

(h : ∀ g : G, 0 < orderOf g) : exponent G = 0 ↔ (Set.range (orderOf : G → ℕ)).Infinite

Full source

@[to_additive]
theorem exponent_eq_zero_iff_range_orderOf_infinite (h : ∀ g : G, 0 < orderOf g) :
    exponentexponent G = 0 ↔ (Set.range (orderOf : G → ℕ)).Infinite := by
  have := exponent_ne_zero_iff_range_orderOf_finite h
  rwa [Ne, not_iff_comm, Iff.comm] at this

Zero Exponent Characterization via Infinite Order Range

Informal description

For a monoid $G$ where every element has positive order, the exponent of $G$ is zero if and only if the set of orders of all elements in $G$ is infinite. That is, $\text{exponent}(G) = 0 \leftrightarrow \{\text{orderOf}(g) \mid g \in G\}$ is infinite.

Monoid.lcm_orderOf_eq_exponent theorem

[Fintype G] : (Finset.univ : Finset G).lcm orderOf = exponent G

Full source

@[to_additive]
theorem lcm_orderOf_eq_exponent [Fintype G] : (Finset.univ : Finset G).lcm orderOf = exponent G :=
  Nat.dvd_antisymm
    (lcm_orderOf_dvd_exponent G)
    (exponent_dvd.mpr fun g => Finset.dvd_lcm (Finset.mem_univ g))

Least Common Multiple of Element Orders Equals Exponent in Finite Monoids

Informal description

For a finite monoid $G$, the least common multiple of the orders of all elements in $G$ is equal to the exponent of $G$. That is, $\text{lcm}\{\text{orderOf}(g) \mid g \in G\} = \text{exponent}(G)$.

Monoid.exponent_dvd_of_monoidHom theorem

(e : G →* H) (e_inj : Function.Injective e) : Monoid.exponent G ∣ Monoid.exponent H

Full source

/--
If there exists an injective, multiplication-preserving map from `G` to `H`,
then the exponent of `G` divides the exponent of `H`.
-/
@[to_additive "If there exists an injective, addition-preserving map from `G` to `H`,
then the exponent of `G` divides the exponent of `H`."]
theorem exponent_dvd_of_monoidHom (e : G →* H) (e_inj : Function.Injective e) :
    Monoid.exponentMonoid.exponent G ∣ Monoid.exponent H :=
  exponent_dvd_of_forall_pow_eq_one fun g => e_inj (by
    rw [map_pow, pow_exponent_eq_one, map_one])

Exponent Divisibility under Injective Monoid Homomorphism

Informal description

Let $G$ and $H$ be monoids, and let $e: G \to H$ be an injective monoid homomorphism. Then the exponent of $G$ divides the exponent of $H$.

Monoid.exponent_eq_of_mulEquiv theorem

(e : G ≃* H) : Monoid.exponent G = Monoid.exponent H

Full source

/--
If there exists a multiplication-preserving equivalence between `G` and `H`,
then the exponent of `G` is equal to the exponent of `H`.
-/
@[to_additive "If there exists a addition-preserving equivalence between `G` and `H`,
then the exponent of `G` is equal to the exponent of `H`."]
theorem exponent_eq_of_mulEquiv (e : G ≃* H) : Monoid.exponent G = Monoid.exponent H :=
  Nat.dvd_antisymm
    (exponent_dvd_of_monoidHom e e.injective)
    (exponent_dvd_of_monoidHom e.symm e.symm.injective)

Exponent Equality under Monoid Equivalence: $\text{exponent}(G) = \text{exponent}(H)$

Informal description

If there exists a multiplication-preserving equivalence $e : G \to H$ between two monoids $G$ and $H$, then the exponent of $G$ is equal to the exponent of $H$.

Submonoid.exponent_top theorem

: Monoid.exponent (⊤ : Submonoid G) = Monoid.exponent G

Full source

@[to_additive (attr := simp)]
theorem _root_.Submonoid.exponent_top :
    Monoid.exponent (⊤ : Submonoid G) = Monoid.exponent G :=
  exponent_eq_of_mulEquiv Submonoid.topEquiv

Exponent Equality for Top Submonoid: $\text{exponent}(\top) = \text{exponent}(G)$

Informal description

The exponent of the top submonoid (i.e., the entire monoid $G$) is equal to the exponent of $G$ itself.

Submonoid.pow_exponent_eq_one theorem

{S : Submonoid G} {g : G} (g_in_s : g ∈ S) : g ^ (Monoid.exponent S) = 1

Full source

@[to_additive]
theorem _root_.Submonoid.pow_exponent_eq_one {S : Submonoid G} {g : G} (g_in_s : g ∈ S) :
    g ^ (Monoid.exponent S) = 1 := by
  have := Monoid.pow_exponent_eq_one (⟨g, g_in_s⟩ : S)
  rwa [SubmonoidClass.mk_pow, ← OneMemClass.coe_eq_one] at this

Submonoid Element Raised to Exponent Yields Identity

Informal description

For any submonoid $S$ of a monoid $G$ and any element $g \in S$, raising $g$ to the power of the exponent of $S$ yields the identity element, i.e., $g^{\text{exponent}(S)} = 1$.

Monoid.ExponentExists.of_finite theorem

: ExponentExists G

Full source

@[to_additive]
theorem ExponentExists.of_finite : ExponentExists G := by
  let _inst := Fintype.ofFinite G
  simp only [Monoid.ExponentExists]
  refine ⟨(Finset.univ : Finset G).lcm orderOf, ?_, fun g => ?_⟩
  · simpa [pos_iff_ne_zero, Finset.lcm_eq_zero_iff] using fun x => (_root_.orderOf_pos x).ne'
  · rw [← orderOf_dvd_iff_pow_eq_one, lcm_orderOf_eq_exponent]
    exact order_dvd_exponent g

Existence of Exponent for Finite Monoids

Informal description

For a finite monoid $G$, there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$.

Monoid.exponent_ne_zero_of_finite theorem

: exponent G ≠ 0

Full source

@[to_additive]
theorem exponent_ne_zero_of_finite : exponentexponent G ≠ 0 :=
  ExponentExists.of_finite.exponent_ne_zero

Nonzero Exponent of Finite Monoid

Informal description

For a finite monoid $G$, the exponent of $G$ is nonzero.

Monoid.one_lt_exponent theorem

[Nontrivial G] : 1 < Monoid.exponent G

Full source

@[to_additive AddMonoid.one_lt_exponent]
lemma one_lt_exponent [Nontrivial G] : 1 < Monoid.exponent G := by
  rw [Nat.one_lt_iff_ne_zero_and_ne_one]
  exact ⟨exponent_ne_zero_of_finite, mt exp_eq_one_iff.mp (not_subsingleton G)⟩

Exponent Greater Than One for Nontrivial Monoids

Informal description

For a nontrivial monoid $G$, the exponent of $G$ is strictly greater than $1$.

Monoid.neZero_exponent_of_finite instance

: NeZero <| Monoid.exponent G

Full source

@[to_additive]
instance neZero_exponent_of_finite : NeZero <| Monoid.exponent G :=
  ⟨Monoid.exponent_ne_zero_of_finite⟩

Nonzero Exponent of Finite Monoids

Informal description

For any finite monoid $G$, the exponent of $G$ is a nonzero natural number.

Monoid.exists_orderOf_eq_exponent theorem

(hG : ExponentExists G) : ∃ g : G, orderOf g = exponent G

Full source

@[to_additive]
theorem exists_orderOf_eq_exponent (hG : ExponentExists G) : ∃ g : G, orderOf g = exponent G := by
  have he := hG.exponent_ne_zero
  have hne : (Set.range (orderOf : G → ℕ)).Nonempty := ⟨1, 1, orderOf_one⟩
  have hfin : (Set.range (orderOf : G → ℕ)).Finite := by
    rwa [← exponent_ne_zero_iff_range_orderOf_finite hG.orderOf_pos]
  obtain ⟨t, ht⟩ := hne.csSup_mem hfin
  use t
  apply Nat.dvd_antisymm (order_dvd_exponent _)
  refine Nat.dvd_of_primeFactorsList_subperm he ?_
  rw [List.subperm_ext_iff]
  by_contra! h
  obtain ⟨p, hp, hpe⟩ := h
  replace hp := Nat.prime_of_mem_primeFactorsList hp
  simp only [Nat.primeFactorsList_count_eq] at hpe
  set k := (orderOf t).factorization p with hk
  obtain ⟨g, hg⟩ := hp.exists_orderOf_eq_pow_factorization_exponent G
  suffices orderOf t < orderOf (t ^ p ^ k * g) by
    rw [ht] at this
    exact this.not_le (le_csSup hfin.bddAbove <| Set.mem_range_self _)
  have hpk : p ^ k ∣ orderOf t := Nat.ordProj_dvd _ _
  have hpk' : orderOf (t ^ p ^ k) = orderOf t / p ^ k := by
    rw [orderOf_pow' t (pow_ne_zero k hp.ne_zero), Nat.gcd_eq_right hpk]
  obtain ⟨a, ha⟩ := Nat.exists_eq_add_of_lt hpe
  have hcoprime : (orderOf (t ^ p ^ k)).Coprime (orderOf g) := by
    rw [hg, Nat.coprime_pow_right_iff (pos_of_gt hpe), Nat.coprime_comm]
    apply Or.resolve_right (Nat.coprime_or_dvd_of_prime hp _)
    nth_rw 1 [← pow_one p]
    have : 1 = (Nat.factorization (orderOf (t ^ p ^ k))) p + 1 := by
     rw [hpk', Nat.factorization_div hpk]
     simp [k, hp]
    rw [this]
    -- Porting note: convert made to_additive complain
    apply Nat.pow_succ_factorization_not_dvd (hG.orderOf_pos <| t ^ p ^ k).ne' hp
  rw [(Commute.all _ g).orderOf_mul_eq_mul_orderOf_of_coprime hcoprime, hpk',
    hg, ha, hk, pow_add, pow_add, pow_one, ← mul_assoc, ← mul_assoc,
    Nat.div_mul_cancel, mul_assoc, lt_mul_iff_one_lt_right <| hG.orderOf_pos t, ← pow_succ]
  · exact one_lt_pow₀ hp.one_lt a.succ_ne_zero
  · exact hpk

Existence of Element with Order Equal to Exponent in Monoids

Informal description

If a monoid $G$ has an exponent (i.e., there exists a positive integer $n$ such that $g^n = 1$ for all $g \in G$), then there exists an element $g \in G$ whose order equals the exponent of $G$, i.e., $\text{orderOf}(g) = \text{exponent}(G)$.

Monoid.exponent_eq_iSup_orderOf theorem

(h : ∀ g : G, 0 < orderOf g) : exponent G = ⨆ g : G, orderOf g

Full source

@[to_additive]
theorem exponent_eq_iSup_orderOf (h : ∀ g : G, 0 < orderOf g) :
    exponent G = ⨆ g : G, orderOf g := by
  rw [iSup]
  by_cases ExponentExists G
  case neg he =>
    rw [← exponent_eq_zero_iff] at he
    rw [he, Set.Infinite.Nat.sSup_eq_zero <| (exponent_eq_zero_iff_range_orderOf_infinite h).1 he]
  case pos he =>
    rw [csSup_eq_of_forall_le_of_forall_lt_exists_gt (Set.range_nonempty _)]
    · simp_rw [Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff]
      exact orderOf_le_exponent he
    intro x hx
    obtain ⟨g, hg⟩ := exists_orderOf_eq_exponent he
    rw [← hg] at hx
    simp_rw [Set.mem_range, exists_exists_eq_and]
    exact ⟨g, hx⟩

Exponent as Supremum of Element Orders in Monoids

Informal description

For a monoid $G$ where every element has positive order, the exponent of $G$ is equal to the supremum of the orders of all elements in $G$, i.e., \[ \text{exponent}(G) = \sup_{g \in G} \text{orderOf}(g). \]

Monoid.exponent_eq_iSup_orderOf' theorem

: exponent G = if ∃ g : G, orderOf g = 0 then 0 else ⨆ g : G, orderOf g

Full source

@[to_additive]
theorem exponent_eq_iSup_orderOf' :
    exponent G = if ∃ g : G, orderOf g = 0 then 0 else ⨆ g : G, orderOf g := by
  split_ifs with h
  · obtain ⟨g, hg⟩ := h
    exact exponent_eq_zero_of_order_zero hg
  · have := not_exists.mp h
    exact exponent_eq_iSup_orderOf fun g => Ne.bot_lt <| this g

Exponent as Supremum of Element Orders in Monoids (General Case)

Informal description

The exponent of a monoid $G$ is equal to $0$ if there exists an element $g \in G$ with $\text{orderOf}(g) = 0$ (i.e., infinite order). Otherwise, the exponent is equal to the supremum of the orders of all elements in $G$, i.e., \[ \text{exponent}(G) = \sup_{g \in G} \text{orderOf}(g). \]

Monoid.exponent_eq_max'_orderOf theorem

[Fintype G] : exponent G = ((@Finset.univ G _).image orderOf).max' ⟨1, by simp⟩

Full source

@[to_additive]
theorem exponent_eq_max'_orderOf [Fintype G] :
    exponent G = ((@Finset.univ G _).image orderOf).max' ⟨1, by simp⟩ := by
  rw [← Finset.Nonempty.csSup_eq_max', Finset.coe_image, Finset.coe_univ, Set.image_univ, ← iSup]
  exact exponent_eq_iSup_orderOf orderOf_pos

Exponent as Maximum Element Order in Finite Monoids

Informal description

For a finite monoid $G$, the exponent of $G$ is equal to the maximum order of its elements, i.e., \[ \text{exponent}(G) = \max_{g \in G} \text{orderOf}(g). \]

Group.exponent_dvd_card theorem

[Fintype G] : Monoid.exponent G ∣ Fintype.card G

Full source

@[to_additive]
theorem Group.exponent_dvd_card [Fintype G] : Monoid.exponentMonoid.exponent G ∣ Fintype.card G :=
  Monoid.exponent_dvd.mpr <| fun _ => orderOf_dvd_card

Exponent Divides Group Order for Finite Groups

Informal description

For any finite group $G$, the exponent of $G$ divides the cardinality of $G$.

Group.exponent_dvd_nat_card theorem

: Monoid.exponent G ∣ Nat.card G

Full source

@[to_additive]
theorem Group.exponent_dvd_nat_card : Monoid.exponentMonoid.exponent G ∣ Nat.card G :=
  Monoid.exponent_dvd.mpr orderOf_dvd_natCard

Exponent Divides Group Cardinality

Informal description

For any group $G$, the exponent of $G$ divides the cardinality of $G$ (when $G$ is considered as a type).

Subgroup.exponent_toSubmonoid theorem

(H : Subgroup G) : Monoid.exponent H.toSubmonoid = Monoid.exponent H

Full source

@[to_additive]
theorem Subgroup.exponent_toSubmonoid (H : Subgroup G) :
    Monoid.exponent H.toSubmonoid = Monoid.exponent H :=
  Monoid.exponent_eq_of_mulEquiv (MulEquiv.subgroupCongr rfl)

Exponent Equality for Subgroup and Submonoid

Informal description

For any subgroup $H$ of a group $G$, the exponent of $H$ considered as a submonoid is equal to the exponent of $H$ as a subgroup. That is, $\text{exponent}(H_{\text{submonoid}}) = \text{exponent}(H)$.

Subgroup.exponent_top theorem

: Monoid.exponent (⊤ : Subgroup G) = Monoid.exponent G

Full source

@[to_additive (attr := simp)]
theorem Subgroup.exponent_top : Monoid.exponent (⊤ : Subgroup G) = Monoid.exponent G :=
  Monoid.exponent_eq_of_mulEquiv topEquiv

Exponent of Top Subgroup Equals Exponent of Group

Informal description

The exponent of the top subgroup (i.e., the entire group $G$) is equal to the exponent of $G$ itself.

Subgroup.pow_exponent_eq_one theorem

{H : Subgroup G} {g : G} (g_in_H : g ∈ H) : g ^ Monoid.exponent H = 1

Full source

@[to_additive]
theorem Subgroup.pow_exponent_eq_one {H : Subgroup G} {g : G} (g_in_H : g ∈ H) :
    g ^ Monoid.exponent H = 1 := exponent_toSubmonoid H ▸ Submonoid.pow_exponent_eq_one g_in_H

Subgroup Element Raised to Exponent Yields Identity

Informal description

For any subgroup $H$ of a group $G$ and any element $g \in H$, raising $g$ to the power of the exponent of $H$ yields the identity element, i.e., $g^{\text{exponent}(H)} = 1$.

Group.exponent_dvd_iff_forall_zpow_eq_one theorem

: (Monoid.exponent G : ℤ) ∣ n ↔ ∀ g : G, g ^ n = 1

Full source

@[to_additive]
theorem Group.exponent_dvd_iff_forall_zpow_eq_one :
    (Monoid.exponent G : ℤ) ∣ n(Monoid.exponent G : ℤ) ∣ n ↔ ∀ g : G, g ^ n = 1 := by
  simp_rw [Int.natCast_dvd, Monoid.exponent_dvd_iff_forall_pow_eq_one, pow_natAbs_eq_one]

Divisibility of Exponent Characterizes Identity Powers in Groups

Informal description

For a group $G$ with exponent $e$, an integer $n$ is divisible by $e$ if and only if for every element $g \in G$, the $n$-th power of $g$ equals the identity element, i.e., $g^n = 1$.

Group.exponent_dvd_sub_iff_zpow_eq_zpow theorem

: (Monoid.exponent G : ℤ) ∣ n - m ↔ ∀ g : G, g ^ n = g ^ m

Full source

@[to_additive]
theorem Group.exponent_dvd_sub_iff_zpow_eq_zpow :
    (Monoid.exponent G : ℤ) ∣ n - m(Monoid.exponent G : ℤ) ∣ n - m ↔ ∀ g : G, g ^ n = g ^ m := by
  simp_rw [Group.exponent_dvd_iff_forall_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Divisibility of Exponent Characterizes Equal Powers in Groups: $e \mid (n - m) \leftrightarrow \forall g \in G, g^n = g^m$

Informal description

For a group $G$ with exponent $e$, the difference $n - m$ is divisible by $e$ if and only if for every element $g \in G$, the $n$-th power of $g$ equals the $m$-th power of $g$, i.e., $g^n = g^m$.

Monoid.exponent_pi_eq_zero theorem

 {ι : Type*} {M : ι → Type*} [∀ i, Monoid (M i)] {j : ι} (hj : exponent (M j) = 0) : exponent ((i : ι) → M i) = 0

Full source

@[to_additive]
theorem Monoid.exponent_pi_eq_zero {ι : Type*} {M : ι → Type*} [∀ i, Monoid (M i)] {j : ι}
    (hj : exponent (M j) = 0) : exponent ((i : ι) → M i) = 0 := by
  classical
  rw [@exponent_eq_zero_iff, ExponentExists] at hj ⊢
  push_neg at hj ⊢
  peel hj with n hn _
  obtain ⟨m, hm⟩ := this
  refine ⟨Pi.mulSingle j m, fun h ↦ hm ?_⟩
  simpa using congr_fun h j

Exponent of Product Monoid Vanishes When a Factor's Exponent Vanishes

Informal description

Let $\{M_i\}_{i \in \iota}$ be a family of monoids indexed by a type $\iota$, and suppose there exists an index $j \in \iota$ such that the exponent of $M_j$ is zero. Then the exponent of the product monoid $\prod_{i \in \iota} M_i$ is also zero.

MonoidHom.exponent_dvd theorem

 {F M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {f : F}
  (hf : Function.Surjective f) : exponent M₂ ∣ exponent M₁

Full source

/-- If `f : M₁ →⋆ M₂` is surjective, then the exponent of `M₂` divides the exponent of `M₁`. -/
@[to_additive]
theorem MonoidHom.exponent_dvd {F M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂]
    [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂]
    {f : F} (hf : Function.Surjective f) : exponentexponent M₂ ∣ exponent M₁ := by
  refine Monoid.exponent_dvd_of_forall_pow_eq_one fun m₂ ↦ ?_
  obtain ⟨m₁, rfl⟩ := hf m₂
  rw [← map_pow, pow_exponent_eq_one, map_one]

Exponent Divisibility Under Surjective Homomorphism: $\text{exponent}(M_2) \mid \text{exponent}(M_1)$

Informal description

Let $M_1$ and $M_2$ be monoids, and let $f: M_1 \to M_2$ be a surjective monoid homomorphism. Then the exponent of $M_2$ divides the exponent of $M_1$, i.e., $\text{exponent}(M_2) \mid \text{exponent}(M_1)$.

Monoid.exponent_pi theorem

 {ι : Type*} [Fintype ι] {M : ι → Type*} [∀ i, Monoid (M i)] : exponent ((i : ι) → M i) = lcm univ (exponent <| M ·)

Full source

/-- The exponent of finite product of monoids is the `Finset.lcm` of the exponents of the
constituent monoids. -/
@[to_additive "The exponent of finite product of additive monoids is the `Finset.lcm` of the
exponents of the constituent additive monoids."]
theorem Monoid.exponent_pi {ι : Type*} [Fintype ι] {M : ι → Type*} [∀ i, Monoid (M i)] :
    exponent ((i : ι) → M i) = lcm univ (exponent <| M ·) := by
  refine dvd_antisymm ?_ ?_
  · refine exponent_dvd_of_forall_pow_eq_one fun m ↦ ?_
    ext i
    rw [Pi.pow_apply, Pi.one_apply, ← orderOf_dvd_iff_pow_eq_one]
    apply dvd_trans (Monoid.order_dvd_exponent (m i))
    exact Finset.dvd_lcm (mem_univ i)
  · apply Finset.lcm_dvd fun i _ ↦ ?_
    exact MonoidHom.exponent_dvd (f := Pi.evalMonoidHom (M ·) i) (Function.surjective_eval i)

Exponent of Product Monoid Equals LCM of Exponents

Informal description

Let $\{M_i\}_{i \in \iota}$ be a finite family of monoids indexed by a finite type $\iota$. The exponent of the product monoid $\prod_{i \in \iota} M_i$ is equal to the least common multiple of the exponents of the monoids $M_i$ for $i \in \iota$, i.e., \[ \text{exponent}\left(\prod_{i \in \iota} M_i\right) = \text{lcm}_{i \in \iota} (\text{exponent}(M_i)). \]

Monoid.exponent_prod theorem

{M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] : exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂)

Full source

/-- The exponent of product of two monoids is the `lcm` of the exponents of the
individuaul monoids. -/
@[to_additive AddMonoid.exponent_prod "The exponent of product of two additive monoids is the `lcm`
of the exponents of the individuaul additive monoids."]
theorem Monoid.exponent_prod {M₁ M₂ : Type*} [Monoid M₁] [Monoid M₂] :
    exponent (M₁ × M₂) = lcm (exponent M₁) (exponent M₂) := by
  refine dvd_antisymm ?_ (lcm_dvd ?_ ?_)
  · refine exponent_dvd_of_forall_pow_eq_one fun g ↦ ?_
    ext1
    · rw [Prod.pow_fst, Prod.fst_one, ← orderOf_dvd_iff_pow_eq_one]
      exact dvd_trans (Monoid.order_dvd_exponent (g.1)) <| dvd_lcm_left _ _
    · rw [Prod.pow_snd, Prod.snd_one, ← orderOf_dvd_iff_pow_eq_one]
      exact dvd_trans (Monoid.order_dvd_exponent (g.2)) <| dvd_lcm_right _ _
  · exact MonoidHom.exponent_dvd (f := MonoidHom.fst M₁ M₂) Prod.fst_surjective
  · exact MonoidHom.exponent_dvd (f := MonoidHom.snd M₁ M₂) Prod.snd_surjective

Exponent of Direct Product Equals LCM of Exponents: $\text{exponent}(M_1 \times M_2) = \text{lcm}(\text{exponent}(M_1), \text{exponent}(M_2))$

Informal description

For any two monoids $M_1$ and $M_2$, the exponent of their direct product $M_1 \times M_2$ is equal to the least common multiple of the exponents of $M_1$ and $M_2$, i.e., \[ \text{exponent}(M_1 \times M_2) = \text{lcm}(\text{exponent}(M_1), \text{exponent}(M_2)). \]

orderOf_eq_two_iff theorem

(hG : Monoid.exponent G = 2) {x : G} : orderOf x = 2 ↔ x ≠ 1

Full source

@[to_additive]
lemma orderOf_eq_two_iff (hG : Monoid.exponent G = 2) {x : G} :
    orderOforderOf x = 2 ↔ x ≠ 1 :=
  ⟨by rintro hx rfl; norm_num at hx, orderOf_eq_prime (hG ▸ Monoid.pow_exponent_eq_one x)⟩

Characterization of Order Two Elements in Monoids of Exponent Two

Informal description

Let $G$ be a monoid with exponent $2$. For any element $x \in G$, the order of $x$ is $2$ if and only if $x$ is not the identity element. In other words, $\text{orderOf}(x) = 2 \leftrightarrow x \neq 1$.

Commute.of_orderOf_dvd_two theorem

[IsCancelMul G] (h : ∀ g : G, orderOf g ∣ 2) (a b : G) : Commute a b

Full source

@[to_additive]
theorem Commute.of_orderOf_dvd_two [IsCancelMul G] (h : ∀ g : G, orderOforderOf g ∣ 2) (a b : G) :
    Commute a b := by
  simp_rw [orderOf_dvd_iff_pow_eq_one] at h
  rw [commute_iff_eq, ← mul_right_inj a, ← mul_left_inj b]
  -- We avoid `group` here to minimize imports while low in the hierarchy;
  -- typically it would be better to invoke the tactic.
  calc
    a * (a * b) * b = a ^ 2 * b ^ 2 := by simp [pow_two, mul_assoc]
    _ = 1 := by rw [h, h, mul_one]
    _ = (a * b) ^ 2 := by rw [h]
    _ = a * (b * a) * b := by simp [pow_two, mul_assoc]

Commutativity from Elements of Order Dividing Two

Informal description

Let $ G $ be a monoid with the left and right cancellation property. If for every element $ g \in G $, the order of $ g $ divides 2, then any two elements $ a, b \in G $ commute, i.e., $ a * b = b * a $.

mul_comm_of_exponent_two theorem

[IsCancelMul G] (hG : Monoid.exponent G = 2) (a b : G) : a * b = b * a

Full source

/-- In a cancellative monoid of exponent two, all elements commute. -/
@[to_additive]
lemma mul_comm_of_exponent_two [IsCancelMul G] (hG : Monoid.exponent G = 2) (a b : G) :
    a * b = b * a :=
  Commute.of_orderOf_dvd_two (fun g => hG ▸ Monoid.order_dvd_exponent g) a b

Commutativity in Cancellative Monoids of Exponent Two

Informal description

Let $G$ be a cancellative monoid with exponent $2$. Then for any two elements $a, b \in G$, we have $a \cdot b = b \cdot a$.

commMonoidOfExponentTwo abbrev

[IsCancelMul G] (hG : Monoid.exponent G = 2) : CommMonoid G

Full source

/-- Any cancellative monoid of exponent two is abelian. -/
@[to_additive "Any additive group of exponent two is abelian."]
abbrev commMonoidOfExponentTwo [IsCancelMul G] (hG : Monoid.exponent G = 2) : CommMonoid G where
  mul_comm := mul_comm_of_exponent_two hG

Cancellative Monoid of Exponent Two is Commutative

Informal description

Let $G$ be a cancellative monoid with exponent $2$. Then $G$ is a commutative monoid.

inv_eq_self_of_exponent_two theorem

(hG : Monoid.exponent G = 2) (x : G) : x⁻¹ = x

Full source

/-- In a group of exponent two, every element is its own inverse. -/
@[to_additive]
lemma inv_eq_self_of_exponent_two (hG : Monoid.exponent G = 2) (x : G) :
    x⁻¹ = x :=
  inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hG ▸ Monoid.pow_exponent_eq_one x

Self-Inverse Property in Monoids of Exponent Two

Informal description

In a monoid $G$ with exponent $2$, every element $x \in G$ satisfies $x^{-1} = x$.

inv_eq_self_of_orderOf_eq_two theorem

{x : G} (hx : orderOf x = 2) : x⁻¹ = x

Full source

/-- If an element in a group has order two, then it is its own inverse. -/
@[to_additive]
lemma inv_eq_self_of_orderOf_eq_two {x : G} (hx : orderOf x = 2) :
    x⁻¹ = x :=
  inv_eq_of_mul_eq_one_left <| pow_two (a := x) ▸ hx ▸ pow_orderOf_eq_one x

Self-Inverse Property for Elements of Order Two

Informal description

For any element $x$ in a group $G$ with order $2$, the inverse of $x$ is equal to itself, i.e., $x^{-1} = x$.

mul_not_mem_of_orderOf_eq_two theorem

{x y : G} (hx : orderOf x = 2) (hy : orderOf y = 2) (hxy : x ≠ y) : x * y ∉ ({ x, y, 1 } : Set G)

Full source

@[to_additive]
lemma mul_not_mem_of_orderOf_eq_two {x y : G} (hx : orderOf x = 2)
    (hy : orderOf y = 2) (hxy : x ≠ y) : x * y ∉ ({x, y, 1} : Set G) := by
  simp only [Set.mem_singleton_iff, Set.mem_insert_iff, mul_eq_left, mul_eq_right,
    mul_eq_one_iff_eq_inv, inv_eq_self_of_orderOf_eq_two hy, not_or]
  aesop

Product of Distinct Order-Two Elements Excludes Original Elements and Identity

Informal description

For any two distinct elements $x$ and $y$ in a group $G$ with orders equal to $2$, their product $x * y$ does not belong to the set $\{x, y, 1\}$.

mul_not_mem_of_exponent_two theorem

(h : Monoid.exponent G = 2) {x y : G} (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) : x * y ∉ ({ x, y, 1 } : Set G)

Full source

@[to_additive]
lemma mul_not_mem_of_exponent_two (h : Monoid.exponent G = 2) {x y : G}
    (hx : x ≠ 1) (hy : y ≠ 1) (hxy : x ≠ y) : x * y ∉ ({x, y, 1} : Set G) :=
  mul_not_mem_of_orderOf_eq_two (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one x) hx)
    (orderOf_eq_prime (h ▸ Monoid.pow_exponent_eq_one y) hy) hxy

Product Exclusion in Exponent-Two Monoids: $x * y \notin \{x, y, 1\}$ for distinct non-identity elements

Informal description

Let $G$ be a monoid with exponent equal to 2. For any two distinct non-identity elements $x, y \in G$, their product $x * y$ does not belong to the set $\{x, y, 1\}$.

Mathlib.GroupTheory.Exponent

Main definitions

Main results

TODO