Advanced linear algebra

The symmetric matrix $A = \begin{pmatrix} 5 & 2 \\ 2 & 2 \end{pmatrix}$ is the matrix of $q(x, y) = 5x^2 + 4xy + 2y^2$. What is the largest eigenvalue of $A$, that is, the maximum of $q$ on the unit circle?

Which of these matrices are unitarily (or, for real ones, orthogonally) diagonalisable over $\mathbb{C}$? (Choose all that apply.)

In the proof of the spectral theorem, $v_1$ is an eigenvector of the self-adjoint operator $T$ and $W = v_1^{\perp}$. Why does $T$ map $W$ into $W$?

A nilpotent operator $N$ on a $5$-dimensional space has $\operatorname{rank} N = 3$, $\operatorname{rank} N^2 = 1$ and $N^3 = 0$. What is the degree of its minimal polynomial?

Let $V$ and $W$ be finite-dimensional. Which statements about $V \otimes W$ are true? (Choose all that apply.)

Let $V = W = \mathbb{R}$ and let $\eta : \mathbb{R} \to \mathbb{R}^*$ be the 'basis' isomorphism sending $1$ to the functional $1^*$ with $1^*(t) = t$. Let $f : \mathbb{R} \to \mathbb{R}$ be $f(t) = 2t$. Compute the number $\big(f^*(\eta(f(1)))\big)(1)$. (Naturality would require it to equal $\eta(1)(1) = 1$.)

Which Lean statement correctly formalises Lemma 2 (eigenvectors of a symmetric operator for distinct eigenvalues are orthogonal)? In each, T : E →ₗ[ℝ] E on a real inner product space E.

What is $\dim\big(\mathbb{R}^3 \otimes \mathbb{R}^4 \otimes \mathbb{R}^2\big)$?

Implement the uniqueness part of Theorem 12. Write block_sizes(ranks) where ranks = [r0, r1, r2, ...] lists $\operatorname{rank}(A - \lambda I)^k$ for $k = 0, 1, 2, \dots$, ending once the ranks stop changing. Return the list of Jordan block sizes for $\lambda$, largest first. (Blocks of size $\geq k$ number $r_{k-1} - r_k$.)