Theorems · Theorem · group theory

Finsupp.mapRange_sub

∀ {ι : Type u_1} {G : Type u_6} {H : Type u_7} [inst : SubNegZeroMonoid G] [inst_1 : SubNegZeroMonoid H] {f : G → H}
  {hf : f 0 = 0},
  (∀ (x y : G), f (x - y) = f x - f y) →
    ∀ (v₁ v₂ : ι →₀ G), Finsupp.mapRange f hf (v₁ - v₂) = Finsupp.mapRange f hf v₁ - Finsupp.mapRange f hf v₂

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

SubNegZeroMonoidSubNegZeroMonoid