Theorems · Theorem · group theory

AddCon.list_sum

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

Additive congruence relations preserve sum indexed by a list.

Defined in

Mathlib.GroupTheory.Congruence.BigOperators

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

AddZeroClass