Theorem QuadraticAlgebra.coe_eq_one_iff

Modification history

2025-12-16 09:36
Mathlib/Algebra/QuadraticAlgebra/Defs.lean
chore: remove QuadraticAlgebra.coe (#32797) …
Deleted QuadraticAlgebra.coe_eq_one_iffView on Github →
2025-11-01 12:56
Mathlib/Algebra/QuadraticAlgebra.lean
feat(Mathlib/Algebra/QuadraticAlgebra): norm, star structure on quadratic alg. (#30059) …
Added QuadraticAlgebra.coe_eq_one_iffView on Github →