inverse_pow — Mathlib

English

For any r in a monoid with zero, and any natural n, the inverse of r^n equals (inverse r)^n.

Русский

Для любого r в моноиде с нулём и любого натурального n обратное к r^n равно (обратное r)^n.

LaTeX

$$$(\text{Ring.inverse } r)^n = \text{Ring.inverse}(r^n)$$$

Lean4

theorem inverse_pow (r : M₀) : ∀ n : ℕ, Ring.inverse r ^ n = Ring.inverse (r ^ n)
  | 0 => by rw [pow_zero, pow_zero, Ring.inverse_one]
  | n + 1 => by rw [pow_succ', pow_succ, Ring.mul_inverse_rev' ((Commute.refl r).pow_left n), Ring.inverse_pow r n]

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