Theorems · Definition · general algebraic systems

DFinsupp.mapRange.addMonoidHom

{ι : Type u} →
  {β₁ : ι → Type v₁} →
    {β₂ : ι → Type v₂} →
      [inst : (i : ι) → AddZeroClass (β₁ i)] →
        [inst_1 : (i : ι) → AddZeroClass (β₂ i)] → ((i : ι) → β₁ i →+ β₂ i) → (Π₀ (i : ι), β₁ i) →+ Π₀ (i : ι), β₂ i

DFinsupp.mapRange as an AddMonoidHom.

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

7 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddZeroClass