Theorems · Definition · ring theory

DirectSum.gMulLHom

{ι : Type uι} →
  (R : Type uR) →
    (A : ι → Type uA) →
      [inst : CommSemiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [inst_2 : (i : ι) → Module R (A i)] →
            [inst_3 : AddMonoid ι] →
              [inst_4 : DirectSum.GSemiring A] → [DirectSum.GAlgebra R A] → {i j : ι} → A i →ₗ[R] A j →ₗ[R] A (i + j)

The piecewise multiplication from the Mul instance, as a bundled linear map. This is the graded version of LinearMap.mul, and the linear version of DirectSum.gMulHom

Defined in

Mathlib.Algebra.DirectSum.Algebra

Cited by

1 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Quot.sound

Assumes

CommSemiringAddCommMonoidModuleAddMonoidDirectSum.GSemiringDirectSum.GAlgebra