Theorem QuadraticAlgebra.coe_ofNat

Modification history

2025-12-16 09:36
Mathlib/Algebra/QuadraticAlgebra/Defs.lean
chore: remove QuadraticAlgebra.coe (#32797) …
Deleted QuadraticAlgebra.coe_ofNatView on Github →
2025-09-05 19:23
Mathlib/Algebra/QuadraticAlgebra.lean
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras (#27511) …
Added QuadraticAlgebra.coe_ofNatView on Github →