Theorem QuadraticAlgebra.algebraMap_eq

Modification history

2026-10-02 10:35
Mathlib/Algebra/QuadraticAlgebra/Defs.lean
chore(Algebra/QuadraticAlgebra): make C the simp normal form (#44417) …
Modified QuadraticAlgebra.algebraMap_eqView on Github →
2025-09-05 19:23
Mathlib/Algebra/QuadraticAlgebra.lean
feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras (#27511) …
Added QuadraticAlgebra.algebraMap_eqView on Github →