Theorem QuadraticAlgebra.mk_zero_eq_C

Modification history

2026-10-02 10:35
Mathlib/Algebra/QuadraticAlgebra/Defs.lean
chore(Algebra/QuadraticAlgebra): make C the simp normal form (#44417) …
Added QuadraticAlgebra.mk_zero_eq_CView on Github →