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 _