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 `Finsupp`s by natural numbers.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Author: Vierkantor

Mathlib.lean

@@ -729,8 +729,11 @@ import Mathlib.Algebra.MonoidAlgebra.Degree
 import Mathlib.Algebra.MonoidAlgebra.Division
 import Mathlib.Algebra.MonoidAlgebra.Grading
 import Mathlib.Algebra.MonoidAlgebra.Ideal
+import Mathlib.Algebra.MonoidAlgebra.Lift
 import Mathlib.Algebra.MonoidAlgebra.MapDomain
+import Mathlib.Algebra.MonoidAlgebra.Module
 import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors
+import Mathlib.Algebra.MonoidAlgebra.Opposite
 import Mathlib.Algebra.MonoidAlgebra.Support
 import Mathlib.Algebra.MonoidAlgebra.ToDirectSum
 import Mathlib.Algebra.MvPolynomial.Basic

Mathlib/Algebra/Group/Finsupp.lean

@@ -289,6 +289,10 @@ variable [AddMonoid M]
 unless `F i`'s addition is commutative. -/
 instance instNatSMul : SMul ℕ (ι →₀ M) where smul n v := v.mapRange (n • ·) (nsmul_zero _)
 
+@[simp, norm_cast] lemma coe_nsmul (n : ℕ) (f : ι →₀ M) : ⇑(n • f) = n • ⇑f := rfl
+
+lemma nsmul_apply (n : ℕ) (f : ι →₀ M) (x : ι) : (n • f) x = n • f x := rfl
+
 instance instAddMonoid : AddMonoid (ι →₀ M) :=
   fast_instance% DFunLike.coe_injective.addMonoid _ coe_zero coe_add fun _ _ => rfl
 

Mathlib/Algebra/MonoidAlgebra/Basic.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Algebra.Equiv
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.MonoidAlgebra.MapDomain
+import Mathlib.Algebra.MonoidAlgebra.Module
 import Mathlib.Data.Finsupp.SMul
 import Mathlib.LinearAlgebra.Finsupp.SumProd