The discriminant of a matrix

noncomputable def Matrix.discr {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.discr = A.charpoly.discr

@[simp]

theorem Matrix.discr_conj {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (g : GL n R) (m : Matrix n n R) : (↑g * m * (↑g)⁻¹).discr = m.discr

@[simp]

theorem Matrix.discr_conj' {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (g : GL n R) (m : Matrix n n R) : ((↑g)⁻¹ * m * ↑g).discr = m.discr

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

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