Theorem QuadraticAlgebra.nonempty_algEquiv_int_iff_discr_eq

Modification history

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