Theorem QuadraticAlgebra.discr_ediv_emod

Modification history

2026-09-25 09:51
Mathlib/Algebra/QuadraticAlgebra/Discriminant.lean
feat(Algebra/QuadraticAlgebra): quadratic algebras over ℤ (#42298) …
Added QuadraticAlgebra.discr_ediv_emodView on Github →