Theorem QuadraticAlgebra.mul_coe_eq_smul

Modification history

2025-12-16 09:36

Mathlib/Algebra/QuadraticAlgebra/Defs.lean

chore: remove QuadraticAlgebra.coe (#32797) …

Deleted QuadraticAlgebra.mul_coe_eq_smul View on Github →

2025-09-05 19:23

Mathlib/Algebra/QuadraticAlgebra.lean

feat(Algebra/QuadraticAlgebra): custom structure for quadratic algebras (#27511) …

Added QuadraticAlgebra.mul_coe_eq_smul View on Github →