inverse_zero — Mathlib

English

The inverse of the zero continuous linear map is the zero map.

Русский

Обратная нулевого непрерывного линейного отображения равна нулю.

LaTeX

$$$ (0 : M \to_L[R] M_2)^{-1} = 0 $$$

Lean4

@[simp]
theorem inverse_zero : inverse (0 : M →L[R] M₂) = 0 :=
  by
  by_cases h : IsInvertible (0 : M →L[R] M₂)
  · rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩
    ext x
    exact Subsingleton.elim _ _
  · exact inverse_of_not_isInvertible h

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