English
For w and v with w: m → K and v: n → K over a field K, the rank of the associated vecMulVec linear form is at most 1.
Русский
Для w: m→K и v: n→K над полем K, соответствующая линейная форма vecMulVec имеет ранг не более 1.
LaTeX
$$$ (\mathrm{vecMulVec}\ w\ v)^{\mathrm{toLin}'}\operatorname{rank} \le 1. $$$
Lean4
theorem rank_vecMulVec.{u} {K m n : Type u} [CommRing K] [Fintype n] [DecidableEq n] (w : m → K) (v : n → K) :
(Matrix.vecMulVec w v).toLin'.rank ≤ 1 := by
nontriviality K
rw [Matrix.vecMulVec_eq (Fin 1), Matrix.toLin'_mul]
refine le_trans (LinearMap.rank_comp_le_left _ _) ?_
refine (LinearMap.rank_le_domain _).trans_eq ?_
rw [rank_fun', Fintype.card_ofSubsingleton, Nat.cast_one]
