The norm along a line and the reversed characteristic polynomial

For an R-algebra S, possibly noncommutative, with a finite basis b and an element w : S, the norm of 1 - t w is the reversed characteristic polynomial det (1 - X M) evaluated at t, where M is the matrix of left multiplication by w. This turns the norm restricted to the line t ↦ 1 - t w into a polynomial in t whose low-degree coefficients are known: its constant term is 1 and its linear coefficient is -tr M.

Main results

• TauCeti.Algebra.eval_charpolyRev_leftMulMatrix: along the line t ↦ 1 - t w, the norm is the reversed characteristic polynomial of multiplication by w.

theorem TauCeti.Algebra.eval_charpolyRev_leftMulMatrix {R : Type u_1} {S : Type u_2} [CommRing R] [Ring S] [Algebra R S] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R S) (w : S) (t : R) : Polynomial.eval t ((Algebra.leftMulMatrix b) w).charpolyRev = (Algebra.norm R) (1 - t • w)

The norm along the line t ↦ 1 - t w is the reversed characteristic polynomial det (1 - X M) of the matrix M of left multiplication by w, evaluated at t.