inv_inv — Mathlib

English

The inverse of the inverse returns the original element, provided fst x ≠ 0.

Русский

Обратное к обратному возвращает исходный элемент при условии fst x ≠ 0.

LaTeX

$$$ fst(x) \\neq 0 \\Rightarrow x^{-1^{-1}} = x $$$

Lean4

protected theorem inv_inv {x : tsze R M} (hx : fst x ≠ 0) : x⁻¹⁻¹ = x :=
  -- adapted from `Matrix.nonsing_inv_nonsing_inv`

  calc
    x⁻¹⁻¹ = 1 * x⁻¹⁻¹ := by rw [one_mul]
    _ = x * x⁻¹ * x⁻¹⁻¹ := by rw [TrivSqZeroExt.mul_inv_cancel hx]
    _ = x := by
      rw [mul_assoc, TrivSqZeroExt.mul_inv_cancel, mul_one]
      rw [fst_inv]
      apply inv_ne_zero hx

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