Theorems · Theorem · group theory

AddCon.multiset_sum

∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (c : AddCon M) {s : Multiset ι} {f g : ι → M},
  (∀ x ∈ s, c (f x) (g x)) → c (Multiset.map f s).sum (Multiset.map g s).sum

Additive congruence relations preserve sum indexed by a multiset.

Defined in

Mathlib.GroupTheory.Congruence.BigOperators

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddCommMonoid