Theorem Algebra.norm_quadraticAlgebra_apply

Modification history

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