Theorems · Theorem · linear algebra

charpoly_leftMulMatrix

∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : Ring S] [inst_2 : Algebra R S] (h : PowerBasis R S),
  ((Algebra.leftMulMatrix h.basis) h.gen).charpoly = minpoly R h.gen

The characteristic polynomial of the map fun x => a * x is the minimal polynomial of a. In combination with det_eq_sign_charpoly_coeff or trace_eq_neg_charpoly_coeff and a bit of rewriting, this will allow us to conclude the field norm resp. trace of x is the product resp. sum of x's conjugates.

Defined in

Mathlib.LinearAlgebra.Matrix.Charpoly.Minpoly

Cited by

2 results in Mathlib

Foundations

Depth 126 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra