English
If u and v are vectors, then the matrix vecMulVec(u,v) has rank at most 1, and its characteristic polynomial is X^n − (u·v) X^{n−1}, where n is the dimension.
Русский
Пусть u и v — векторы размерности n. Матрица vecMulVec(u,v) имеет ранга не более 1, и её характеристический многочлен равен $X^n - (u\\cdot v) X^{n-1}$, где n — размерность.
LaTeX
$$$$ \\operatorname{charpoly}\\big(\\operatorname{vecMulVec}(u,v)\\big) = X^{|n|} - (u \\cdot v) \\; X^{|n|-1}. $$$$
Lean4
theorem charpoly_vecMulVec (u v : n → R) :
(vecMulVec u v).charpoly = X ^ Fintype.card n - (u ⬝ᵥ v) • X ^ (Fintype.card n - 1) :=
by
cases isEmpty_or_nonempty n
· simp
· have h : 1 ≤ Fintype.card n := NeZero.one_le
rw [vecMulVec_eq (ι := Unit), charpoly_mul_comm_of_le (n := Unit) _ _ h, charpoly, charmatrix]
simp [-Matrix.map_mul, mul_sub, ← pow_succ, h, dotProduct_comm, smul_eq_C_mul]
