nonsing_inv_nonsing_inv — Mathlib

English

For A with invertible determinant, (A⁻¹)⁻¹ = A.

Русский

При детерминанте A, обращаемой детерминантной, (A⁻¹)⁻¹ = A.

LaTeX

$$$\text{If } \det A \text{ is a unit, then } (A^{-1})^{-1}=A.$$$

Lean4

@[simp]
theorem nonsing_inv_nonsing_inv (h : IsUnit A.det) : A⁻¹⁻¹ = A :=
  calc
    A⁻¹⁻¹ = 1 * A⁻¹⁻¹ := by rw [Matrix.one_mul]
    _ = A * A⁻¹ * A⁻¹⁻¹ := by rw [A.mul_nonsing_inv h]
    _ = A := by rw [Matrix.mul_assoc, A⁻¹.mul_nonsing_inv (A.isUnit_nonsing_inv_det h), Matrix.mul_one]

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