inverse_eq_inv' — Mathlib

English

In a ring with zero, the Ring.inverse operation coincides with the standard inverse: for all x, Ring.inverse x = x^{-1}.

Русский

В кольце с нулём операция Ring.inverse совпадает с обычной обратной: для всех x выполняется Ring.inverse x = x^{-1}.

LaTeX

$$$\forall x\in G_0:\; \text{Ring.inverse}(x) = x^{-1}$$$

Lean4

@[simp]
theorem inverse_eq_inv' : (Ring.inverse : G₀ → G₀) = Inv.inv :=
  funext Ring.inverse_eq_inv

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