Theorems · Definition · ring theory

DirectSum.mulHom

{ι : Type u_1} →
  [DecidableEq ι] →
    (A : ι → Type u_2) →
      [inst : Add ι] →
        [inst_1 : (i : ι) → AddCommMonoid (A i)] →
          [DirectSum.GNonUnitalNonAssocSemiring A] →
            (DirectSum ι fun i => A i) →+ (DirectSum ι fun i => A i) →+ DirectSum ι fun i => A i

The multiplication from the Mul instance, as a bundled homomorphism.

Defined in

Mathlib.Algebra.DirectSum.Ring

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqAddAddCommMonoidDirectSum.GNonUnitalNonAssocSemiring