mul_eq_one_comm_of_equiv — Mathlib

English

There exists a right inverse for A iff A is a unit (alternative formulation).

Русский

Существует правый обратный к A тогда и только тогда, когда A единица.

LaTeX

$$$\exists B: AB=I \iff A \text{ is a unit}$$$

Lean4

/-- A version of `mul_eq_one_comm` that works for square matrices with rectangular types. -/
theorem mul_eq_one_comm_of_equiv {A : Matrix m n R} {B : Matrix n m R} (e : m ≃ n) : A * B = 1 ↔ B * A = 1 :=
  by
  refine (reindex e e).injective.eq_iff.symm.trans ?_
  rw [reindex_apply, reindex_apply, submatrix_one_equiv, ← submatrix_mul_equiv _ _ _ (.refl _), mul_eq_one_comm,
    submatrix_mul_equiv, coe_refl, submatrix_id_id]

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