of_pow_eq_one — Mathlib

English

If ha: a^n = 1 and hn: n ≠ 0, then the unit constructed from a and n powers satisfies a^n = 1.

Русский

Пусть ha: a^n = 1 и hn: n ≠ 0. Тогда единица, связанная с a и степенями, удовлетворяет a^n = 1.

LaTeX

$$$a^n = 1 \\\\land n \\\\neq 0 \\\\Rightarrow \\\\operatorname{IsUnit}(a) \\\\land (a^n = 1)$$$

Lean4

@[to_additive]
theorem of_pow_eq_one (ha : a ^ n = 1) (hn : n ≠ 0) : IsUnit a :=
  (Units.ofPowEqOne _ n ha hn).isUnit

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