pow_eq_mod_exponent — Mathlib

English

Exponent of the opposite monoid equals the exponent of the original monoid.

Русский

Экспонента противоположной моноидной структуры равна экспоненте исходной.

LaTeX

$$$\\operatorname{exponent}(\\mathrm{MulOpposite}\\,G)=\\operatorname{exponent}(G)$$$

Lean4

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

Похожие утверждения