vecMul_surjective_iff_exists_left_inverse

English

Function surjectivity of vecMul is equivalent to existence of a left inverse B with B A = 1.

Русский

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

LaTeX

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

Lean4

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

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