Theorems · Theorem · general algebraic systems

DFinsupp.mapRange.addMonoidHom_apply

∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → AddZeroClass (β₁ i)]
  [inst_1 : (i : ι) → AddZeroClass (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) (x : Π₀ (i : ι), β₁ i),
  (DFinsupp.mapRange.addMonoidHom f) x = DFinsupp.mapRange (fun i x => (f i) x) ⋯ x

Defined in

Mathlib.Data.DFinsupp.Defs

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddZeroClassAddZeroClass