English
If the ambient dimension is at least 2, then the determinant of a rank-1 matrix vecMulVec is zero.
Русский
Если размерность пространства по крайней мере 2, то детерминант матрицы ранга 1 равен нулю.
LaTeX
$$$\\det(\\mathrm{vecMulVec}(u,v)) = 0$$$
Lean4
theorem det_vecMulVec [Nontrivial n] (u v : n → R) : (vecMulVec u v).det = 0 :=
by
obtain ⟨i, j, hij⟩ := exists_pair_ne n
let uv' := ((vecMulVec u v).updateRow i v).updateRow j v
have huv' : uv'.det = 0 := by
refine detRowAlternating.map_eq_zero_of_eq _ ?_ hij
simp [uv', hij]
have : vecMulVec u v = (uv'.updateRow i (u i • uv' i)).updateRow j (u j • uv'.updateRow i (u i • uv' i) j) :=
by
unfold uv'
rw [updateRow_comm _ hij, updateRow_idem, updateRow_ne hij.symm, updateRow_ne hij, updateRow_self, updateRow_self,
updateRow_comm _ hij, updateRow_idem, ← update_vecMulVec u v j, update_eq_self, ← update_vecMulVec u v i,
update_eq_self]
rw [this, det_updateRow_smul, updateRow_eq_self, det_updateRow_smul, updateRow_eq_self, huv', mul_zero, mul_zero]
