Theorems · Theorem · group theory

Finsupp.mapRange_neg

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

Defined in

Mathlib.Algebra.Group.Finsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

NegZeroClassNegZeroClass