Theorem Algebra.discr_quadraticAlgebra

Modification history

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