invertiblePow — Mathlib

English

If m is invertible in a monoid, then every power m^n (n ∈ ℕ) is invertible, and its inverse is (m^{-1})^{n}.

Русский

Если m обратим в моноиде, то всякая степень m^n (n ∈ ℕ) обратима, и её обратное равно (m^{-1})^{n}.

LaTeX

$$$\text{Invertible}(m) \Rightarrow \text{Invertible}(m^n) \quad \text{and} \quad (m^n)^{-1} = (m^{-1})^n$$$

Lean4

instance invertiblePow (m : α) [Invertible m] (n : ℕ) : Invertible (m ^ n)
    where
  invOf := ⅟m ^ n
  invOf_mul_self := by rw [← (commute_invOf m).symm.mul_pow, invOf_mul_self, one_pow]
  mul_invOf_self := by rw [← (commute_invOf m).mul_pow, mul_invOf_self, one_pow]

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