Theorem QuadraticAlgebra.polynomial_discr_eq_discr

Modification history

2026-10-17 12:17
Mathlib/RingTheory/QuadraticAlgebra.lean
feat(RingTheory/QuadraticAlgebra): trace, norm and discriminant as `Algebra` invariants (#42297) …
Added QuadraticAlgebra.polynomial_discr_eq_discrView on Github →