invertibleOfPowEqOne — Mathlib

English

If x^n = 1 with n ≠ 0 in a monoid, then x is invertible and x^{n-1} is its inverse.

Русский

Если в моноиде выполнено x^n = 1 при n ≠ 0, то x обратим и x^{n-1} является его обратным.

LaTeX

$$$(x^n = 1) \land (n \neq 0) \Rightarrow \text{Invertible}(x)$$$

Lean4

/-- If `x ^ n = 1` then `x` has an inverse, `x^(n - 1)`. -/
def invertibleOfPowEqOne (x : α) (n : ℕ) (hx : x ^ n = 1) (hn : n ≠ 0) : Invertible x :=
  (Units.ofPowEqOne x n hx hn).invertible

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