nonsing_inv_cancel_or_zero — Mathlib

English

For any square matrix A over a commutative ring, either det(A) is a unit and A has a two-sided inverse (A⁻¹ is the inverse on both sides), or the inverse defined by the construction is the zero matrix.

Русский

Для любой квадратной матрицы A над коммутативным кольцом либо детерминант A является единицей, и существует двухсторонняя обратная, либо обратная матрица определяется как ноль.

LaTeX

$$$A\in M_n(R)\;\Rightarrow\; (\det A) \text{ единица или не единица}\; \Longrightarrow\; (A^{-1}A=I \land AA^{-1}=I) \lor (A^{-1}=0).$$$

Lean4

theorem nonsing_inv_cancel_or_zero : A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0 :=
  by
  by_cases h : IsUnit A.det
  · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩
  · exact Or.inr (nonsing_inv_apply_not_isUnit _ h)

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