Documentation

Mathlib.LinearAlgebra.Matrix.Charpoly.Disc

The discriminant of a matrix #

source
🔸 coverage
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
      📐 coverage
      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
      📐 coverage
      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
      🔸 coverage
      @[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
          📐 coverage
          @[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
          📐 coverage
          @[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.