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

theorem Matrix.discr_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.discr = A.trace ^ 2 - 4 * A.det

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

@[deprecated Matrix.discr (since := "2025-10-20")]

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

Alias of Matrix.discr.

---

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

Equations

• @Matrix.disc = @Matrix.discr

@[deprecated Matrix.discr_of_card_eq_two (since := "2025-10-20")]

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.discr = A.trace ^ 2 - 4 * A.det

Alias of Matrix.discr_of_card_eq_two.

@[deprecated Matrix.discr_fin_two (since := "2025-10-20")]

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

Alias of Matrix.discr_fin_two.