inv_zero — Mathlib

English

IsUnit A⁻¹ ⇔ IsUnit A, reflecting that invertibility of A and A⁻¹ coincide.

Русский

IsUnit A⁻¹ ⇔ IsUnit A, отражающее совпадение обратимости A и A⁻¹.

LaTeX

$$$\text{IsUnit}(A^{-1}) \iff \text{IsUnit}(A).$$$

Lean4

@[simp]
theorem inv_zero : (0 : Matrix n n α)⁻¹ = 0 :=
  by
  rcases subsingleton_or_nontrivial α with ht | ht
  · simp [eq_iff_true_of_subsingleton]
  rcases (Fintype.card n).zero_le.eq_or_lt with hc | hc
  · rw [eq_comm, Fintype.card_eq_zero_iff] at hc
    subsingleton
  · have hn : Nonempty n := Fintype.card_pos_iff.mp hc
    refine nonsing_inv_apply_not_isUnit _ ?_
    simp

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