pow_ofPowEqOne — Mathlib

English

If a^n = 1 with n ≠ 0, then the unit corresponding to a has nth power equal to 1.

Русский

Если a^n = 1 и n ≠ 0, тогда единица, соответствующая a, имеет n-ную степень равной 1.

LaTeX

$$$a^n = 1 \\\\land n \\\\neq 0 \\\\Rightarrow \\\\text{the unit with value } a \\\\text{ satisfies } u^n = 1$$$

Lean4

@[to_additive (attr := simp)]
theorem pow_ofPowEqOne (ha : a ^ n = 1) (hn : n ≠ 0) : Units.ofPowEqOne _ n ha hn ^ n = 1 :=
  Units.ext <| by simp [ha]

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