Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

The discriminant of a matrix #

source
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
Instances For
    source
    @[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
    source
    @[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
    source
    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
    source
    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
    source
    @[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
    Instances For
      source
      @[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] [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.

      source
      @[deprecated Matrix.discr_fin_two (since := "2025-10-20")]
      theorem Matrix.disc_fin_two {R : Type u_1} [CommRing R] (A : Matrix (Fin 2) (Fin 2) R) :
      A.discr = A.trace ^ 2 - 4 * A.det

      Alias of Matrix.discr_fin_two.