Theorem AddMonoidAlgebra.toDirectSum_single

Modification history

2025-12-12 18:47
Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
chore(Algebra/MonoidAlgebra): reduce dependence on defeq abuse, golf (#32604) …
Modified AddMonoidAlgebra.toDirectSum_singleView on Github →
2023-05-20 15:51
Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
feat: port Algebra.MonoidAlgebra.ToDirectSum (#4087)
Added AddMonoidAlgebra.toDirectSum_singleView on Github →