mul_right_injective_iff_mulVec_injective

English

Same as above: vecMulVec u v * vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x).

Русский

То же самое: vecMulVec u v · vecMulVec w x = vecMulVec u ((v ⬝ᵥ w) • x).

LaTeX

$$$\operatorname{vecMulVec}\, u\, v \; *\; \operatorname{vecMulVec} \ w \ x = \operatorname{vecMulVec} u\big((v \;⬝ᵥ\; w) \;•\; x\big)$$$

Lean4

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

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