Theorems · Definition · general algebraic systems

DFinsupp.mapRange

{ι : Type u} →
  {β₁ : ι → Type v₁} →
    {β₂ : ι → Type v₂} →
      [inst : (i : ι) → Zero (β₁ i)] →
        [inst_1 : (i : ι) → Zero (β₂ i)] →
          (f : (i : ι) → β₁ i → β₂ i) → (∀ (i : ι), f i 0 = 0) → (Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i

The composition of f : β₁ → β₂ and g : Π₀ i, β₁ i is mapRange f hf g : Π₀ i, β₂ i, well defined when f 0 = 0. This preserves the structure on f, and exists in various bundled forms for when f is itself bundled: * DFinsupp.mapRange.addMonoidHom * DFinsupp.mapRange.addEquiv * dfinsupp.mapRange.linearMap * dfinsupp.mapRange.linearEquiv

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

29 results in Mathlib

Foundations

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

Assumes

ZeroZero