Theorems · Theorem · group theory

Con.list_prod

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

Multiplicative congruence relations preserve product 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

MulOneClass