Commit 2026-10-17 12:17 39cb4443

View on Github →

feat(RingTheory/QuadraticAlgebra): trace, norm and discriminant as Algebra invariants (#42297) Add a RingTheory-level file for QuadraticAlgebra R a b, identifying its elementary trace, norm and discriminant with the general Algebra ones on the standard basis {1, ω}. Kept in a separate file so those stay free of the heavy RingTheory.Discriminant import.

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/QuadraticAlgebra.lean

added theorem Algebra.discr_quadraticAlgebra

added theorem Algebra.leftMulMatrix_quadraticAlgebra

added theorem Algebra.norm_quadraticAlgebra_apply

added theorem Algebra.trace_quadraticAlgebra_apply

added theorem QuadraticAlgebra.polynomial_discr_eq_discr