inverse_invertible — Mathlib

English

For any invertible x in a Monoid with zero, Ring.inverse(x) equals x^{-1}.

Русский

Для любого обратимого x в моноиде с нулём Ring.inverse(x) равняется x^{-1}.

LaTeX

$$$\\\\operatorname{Ring.inverse}(x) = x^{-1}$, \\\\text{for } x \\\\text{invertible}. $$$

Lean4

/-- A variant of `Ring.inverse_unit`. -/
@[simp]
theorem inverse_invertible (x : α) [Invertible x] : Ring.inverse x = ⅟x :=
  Ring.inverse_unit (unitOfInvertible _)

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