The discriminant of a matrix

noncomputable def Matrix.disc {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (A : Matrix n n R) : R

The discriminant of a matrix is defined to be the discriminant of its characteristic polynomial.

Equations

• A.disc = A.charpoly.disc

theorem Matrix.disc_of_card_eq_two {R : Type u_1} {n : Type u_2} [CommRing R] [Nontrivial R] [Fintype n] [DecidableEq n] (A : Matrix n n R) (hn : Fintype.card n = 2) : A.disc = A.trace ^ 2 - 4 * A.det

theorem Matrix.disc_fin_two {R : Type u_1} [CommRing R] [Nontrivial R] (A : Matrix (Fin 2) (Fin 2) R) : A.disc = A.trace ^ 2 - 4 * A.det