inverse_unit — Mathlib

English

For a unit u, the multiplicative inverse of its underlying element equals the underlying value of the inverse unit.

Русский

Для единицы u обратное по умножению к её базовому элементу равно базовому значению обратной единицы.

LaTeX

$$$\text{inverse}(u) = ((u^{-1}: M_0^\times): M_0)$$$

Lean4

/-- By definition, if `x` is invertible then `inverse x = x⁻¹`. -/
theorem inverse_unit (u : M₀ˣ) : inverse (u : M₀) = (u⁻¹ : M₀ˣ) := by
  rw [inverse, dif_pos u.isUnit, IsUnit.unit_of_val_units]

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