@[reducible, inline]

noncomputable abbrev mulLeft (K : Type u_1) (L : Type u_2) [CommRing K] [CommRing L] [Algebra K L] (α : L) : L →ₗ[K] L

The $K$-linear map $L \to L$ given by left multiplication by $\alpha \in L$.

noncomputable def traceOfExtension (K : Type u_1) (L : Type u_2) [CommRing K] [CommRing L] [Algebra K L] : L →ₗ[K] K

The trace map $\mathrm{Tr}_{L/K} : L \to K$ of the algebra $L$ over $K$.

noncomputable def normOfExtension (K : Type u_1) (L : Type u_2) [CommRing K] [CommRing L] [Algebra K L] : L →* K

The norm map $\mathrm{N}_{L/K} : L \to K$ of the algebra $L$ over $K$.

theorem Matrix.charpoly_blockDiagonal_const {R : Type u_3} [CommRing R] {n : Type u_4} [DecidableEq n] [Fintype n] {m : Type u_5} [DecidableEq m] [Fintype m] (M : Matrix n n R) : (blockDiagonal fun (x : m) => M).charpoly = M.charpoly ^ Fintype.card m

The characteristic polynomial of a constant block-diagonal matrix is the characteristic polynomial of the block raised to the number of blocks.

theorem charpoly_lmul_eq_minpoly_pow {K : Type u_3} [Field K] {L : Type u_4} [Field L] [Algebra K L] [FiniteDimensional K L] (α : L) (hα_int : IsIntegral K α) : LinearMap.charpoly ((Algebra.lmul K L) α) = minpoly K α ^ (Module.finrank K L / Module.finrank K ↥K⟮α⟯)

For a finite field extension $L/K$ and $\alpha \in L$ integral over $K$, the characteristic polynomial of multiplication by $\alpha$ is the minimal polynomial of $\alpha$ raised to the power $[L:K]/[K(\alpha):K]$.