mul_left_injective_iff_vecMul_injective

English

For any A ∈ M(l,m;α), the right multiplication B ↦ A B is injective if and only if the linear map B ↦ A.mulVec is injective.

Русский

Для A ∈ M(l,m;α) правая инъекция B ↦ AB эквивалентна инъективности линейного отображения B ↦ A.mulVec.

LaTeX

$$Injective( B ↦ A B ) iff Injective( v ↦ A.mulVec v )$$

Lean4

theorem mul_left_injective_iff_vecMul_injective [Nonempty l] [Fintype m] {A : Matrix m n α} :
    Function.Injective (fun B : Matrix l m α => B * A) ↔ Function.Injective A.vecMul :=
  by
  refine ⟨fun ha v w hvw => ?_, fun ha B C hBC => ext_row fun i => ha congr(($hBC).row i)⟩
  inhabit l
  suffices (of fun i j => v j) = (of fun i j => w j) from funext fun j => congrFun₂ this (default : l) j
  exact ha <| ext fun _ _ => congrFun hvw _

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