Theorems · Definition · general algebraic systems

Finsupp.mapRange

{α : Type u_1} →
  {M : Type u_4} → {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → (f : M → N) → f 0 = 0 → (α →₀ M) → α →₀ N

The composition of f : M → N and g : α →₀ M is mapRange f hf g : α →₀ N, which is well-defined when f 0 = 0. This preserves the structure on f, and exists in various bundled forms for when f is itself bundled (defined in Mathlib/Data/Finsupp/Basic.lean): * Finsupp.mapRange.equiv * Finsupp.mapRange.zeroHom * Finsupp.mapRange.addMonoidHom * Finsupp.mapRange.addEquiv * Finsupp.mapRange.linearMap * Finsupp.mapRange.linearEquiv

Defined in

Mathlib.Data.Finsupp.Defs

Cited by

91 results in Mathlib

Foundations

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

Assumes

ZeroZero