mulVec_surjective_iff_exists_right_inverse

English

Function surjectivity of mulVec is equivalent to existence of a right inverse B with A B = 1.

Русский

Сюрьективность mulVec эквивалентна существованию правого обратного $B$ с $A B = 1$.

LaTeX

$$$\text{Surjective } A.vecMul \iff \exists B, A B = 1$$$

Lean4

theorem mulVec_surjective_iff_exists_right_inverse [DecidableEq m] [Finite m] [Fintype n] {A : Matrix m n R} :
    Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 :=
  by
  cases nonempty_fintype m
  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ y, by simp [hBA]⟩⟩
  choose cols hcols using (h <| Pi.single · 1)
  refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
  rw [one_eq_pi_single, Pi.single_comm, ← hcols j]
  rfl

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