Theorems · Theorem · commutative algebra

RingCon.multisetSum

∀ {ι : Type u_1} {S : Type u_2} [inst : AddCommMonoid S] [inst_1 : Mul S] (t : RingCon S) (s : Multiset ι)
  {f g : ι → S}, (∀ i ∈ s, t (f i) (g i)) → t (Multiset.map f s).sum (Multiset.map g s).sum

Congruence relation of a ring preserves finite sum indexed by a multiset.

Defined in

Mathlib.RingTheory.Congruence.BigOperators

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidMul