Theorems · Definition · linear algebra
Matrix.discr
{R : Type u_1} → {n : Type u_2} → [CommRing R] → [Fintype n] → [DecidableEq n] → Matrix n n R → RThe discriminant of a matrix is defined to be the discriminant of its characteristic polynomial.
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommRingFintypeDecidableEq
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Fintypestatement and proof · cited by 7,736
- Matrixstatement and proof · cited by 4,303
- Matrix.charpolyproof · cited by 82
- Polynomial.discrproof · cited by 7
Cited by20
Results whose statement or proof uses this declaration.
- Matrix.discr_fin_twostatement · cited by 12
- Matrix.IsParabolicproof · cited by 10
- Matrix.IsEllipticproof · cited by 9
- Matrix.IsHyperbolicproof · cited by 5
- UpperHalfPlane.fixedPtproof · cited by 4
- Matrix.GeneralLinearGroup.IsParabolic.smul_eq_self_iffproof · cited by 3
- Matrix.discr_conjstatement · cited by 3
- Matrix.sub_scalar_sq_eq_discrstatement · cited by 2
- Matrix.discr_of_card_eq_twostatement and proof · cited by 1
- UpperHalfPlane.gl_smul_eq_self_iff_eq_fixedPtproof · cited by 1
- UpperHalfPlane.isElliptic_of_exists_smul_eq_selfproof · cited by 1
- Matrix.isHyperbolic_conj_iffproof · cited by 1