Commit 2023-05-20 15:51 ebfb60dc

View on Github →

feat: port Algebra.MonoidAlgebra.ToDirectSum (#4087)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

added def AddMonoidAlgebra.toDirectSum

added theorem AddMonoidAlgebra.toDirectSum_add

added theorem AddMonoidAlgebra.toDirectSum_mul

added theorem AddMonoidAlgebra.toDirectSum_single

added theorem AddMonoidAlgebra.toDirectSum_toAddMonoidAlgebra

added theorem AddMonoidAlgebra.toDirectSum_zero

added def DirectSum.toAddMonoidAlgebra

added theorem DirectSum.toAddMonoidAlgebra_add

added theorem DirectSum.toAddMonoidAlgebra_mul

added theorem DirectSum.toAddMonoidAlgebra_of

added theorem DirectSum.toAddMonoidAlgebra_toDirectSum

added theorem DirectSum.toAddMonoidAlgebra_zero

added def addMonoidAlgebraAddEquivDirectSum

added def addMonoidAlgebraAlgEquivDirectSum

added def addMonoidAlgebraEquivDirectSum

added def addMonoidAlgebraRingEquivDirectSum