Theorems · Definition · ring theory

DirectSum.Gmodule.casesOn

{ι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) → AddMonoid (A i)] →
              [inst_3 : (i : ιB) → AddMonoid (M i)] →
                [inst_4 : GradedMonoid.GMonoid A] →
                  {motive : DirectSum.Gmodule A M → Sort u} →
                    (t : DirectSum.Gmodule A M) →
                      ([toGdistribMulAction : DirectSum.GdistribMulAction A M] →
                          (add_smul :
                              ∀ {i : ιA} {j : ιB} (a a' : A i) (b : M j),
                                GradedMonoid.GSMul.smul (a + a') b =
                                  GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a' b) →
                            (zero_smul : ∀ {i : ιA} {j : ιB} (b : M j), GradedMonoid.GSMul.smul 0 b = 0) →
                              motive
                                { toGdistribMulAction := toGdistribMulAction, add_smul := add_smul,
                                  zero_smul := zero_smul }) →
                        motive t

Defined in

Mathlib.Algebra.Module.GradedModule

Cited by

0 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

AddMonoidVAddAddMonoidAddMonoidGradedMonoid.GMonoid