Theorems · Theorem · group theory

Multiset.sum_map_tsub

∀ {ι : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [ExistsAddOfLE M] [AddLeftMono M]
  [AddLeftReflectLE M] [inst_5 : Sub M] [OrderedSub M] (l : Multiset ι) {f g : ι → M},
  (∀ x ∈ l, g x ≤ f x) → (Multiset.map (fun x => f x - g x) l).sum = (Multiset.map f l).sum - (Multiset.map g l).sum

Defined in

Mathlib.Algebra.BigOperators.Group.Multiset.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidPartialOrderExistsAddOfLEAddLeftMonoAddLeftReflectLESubOrderedSub