ofPowEqOne — Mathlib

English

If a^n = 1 and n ≠ 0, then a is a unit and its inverse is a^{n-1}.

Русский

Если a^n = 1 и n ≠ 0, то a — единица, и ее обратное равно a^{n-1}.

LaTeX

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

Lean4

/-- If `a ^ n = 1`, `n ≠ 0`, then `a` is a unit. -/
@[to_additive (attr := simps!) /-- If `n • x = 0`, `n ≠ 0`, then `x` is an additive unit. -/
    ]
def ofPowEqOne (a : M) (n : ℕ) (ha : a ^ n = 1) (hn : n ≠ 0) : Mˣ :=
  Units.ofPow 1 a hn ha

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