multisetSum — Mathlib

English

A RingCon relation t preserves the sum over a finite multiset, i.e., t(∑ f(i)) (∑ g(i)) whenever t(f(i)) (g(i)) for all i in the multiset.

Русский

Отношение RingCon сохраняет сумму по мультисету: если t(f(i)) связано с g(i) для всех i в мультисете, то t(сумма f(i)) связано с суммой g(i).

LaTeX

$$$$ \forall s : Multiset ι, \, (\forall i ∈ s, t (f i) (g i)) \Rightarrow t(\text{sum}_s f) (\text{sum}_s g) $$$$

Lean4

/-- Congruence relation of a ring preserves finite sum indexed by a multiset. -/
protected theorem multisetSum {ι S : Type*} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Multiset ι) {f g : ι → S}
    (h : ∀ i ∈ s, t (f i) (g i)) : t (s.map f).sum (s.map g).sum :=
  t.toAddCon.multiset_sum h

Похожие утверждения