Commit 2025-08-13 12:33 39ad44ac

chore(Algebra/MonoidAlgebra): split Defs.lean further (#28030) This is a resurrection of #19091. This PR further splits the almost-big file MonoidAlgebra/Defs.lean to focus on the ring structure on (Add)MonoidAlgebra. The following files have been split off:

• MonoidAlgebra/Lift.lean: definition of liftNC
• MonoidAlgebra/Module.lean: module structure (and some submodule results)
• MonoidAlgebra/Opposite.lean: results on the MulOpposite ring structure I also changed one proof about scalar multiplication by natural numbers, so that it wouldn't need a full on module structure on Finsupp. This required adding a pair of lemmas on the definition of multiplying Finsupps by natural numbers.