Small lemmas on graded modules

theorem MultiplicativeBasisDeformations.GExt.GMod.act_sum {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) {κ : Type u_4} (s : Finset κ) (f : κ → M) (b : Λ) : (MM.act (∑ i ∈ s, f i)) b = ∑ i ∈ s, (MM.act (f i)) b

theorem MultiplicativeBasisDeformations.GExt.GMod.act_smul {R : Type u_1} [CommRing R] {Λ : Type u_2} [Ring Λ] [Algebra R Λ] {GΛ : GAlg Λ} {M : Type u_3} [AddCommGroup M] [Module R M] (MM : GMod GΛ M) (t : R) (m : M) (b : Λ) : (MM.act (t • m)) b = t • (MM.act m) b