Theorems · Definition · ring theory

DirectSum.Gmodule.smulAddMonoidHom

{ιA : Type u_1} →
  {ιB : Type u_2} →
    (A : ιA → Type u_3) →
      (M : ιB → Type u_4) →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : (i : ιA) → AddCommMonoid (A i)] →
              [inst_3 : (i : ιB) → AddCommMonoid (M i)] →
                [DecidableEq ιA] →
                  [DecidableEq ιB] →
                    [inst_6 : GradedMonoid.GMonoid A] →
                      [DirectSum.Gmodule A M] →
                        (DirectSum ιA fun i => A i) →+ (DirectSum ιB fun i => M i) →+ DirectSum ιB fun i => M i

For graded monoid A and a graded module M over A. Gmodule.smulAddMonoidHom is the ⨁ᵢ Aᵢ-scalar multiplication on ⨁ᵢ Mᵢ induced by gsmul_hom.

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidVAddAddCommMonoidAddCommMonoidDecidableEqDecidableEqGradedMonoid.GMonoidDirectSum.Gmodule