Theorem QuadraticAlgebra.discr_def

Modification history

2026-09-25 09:51
Mathlib/Algebra/QuadraticAlgebra/Discriminant.lean
feat(Algebra/QuadraticAlgebra): quadratic algebras over ℤ (#42298) …
Modified QuadraticAlgebra.discr_defView on Github →
2026-08-13 09:59
Mathlib/Algebra/QuadraticAlgebra/Discr.lean
feat(Algebra/QuadraticAlgebra): discriminant and field criterion (#42206) …
Added QuadraticAlgebra.discr_defView on Github →