list_prod_apply — Mathlib

English

Let α be a type and M a family of monoids indexed by α. For a fixed a ∈ α and a list l of functions f: α → M,

Русский

Пусть α — тип, и M — одинаковые моноиды по индексу α. Пусть a ∈ α и есть список функций f: α → M. Тогда

LaTeX

$$$$ l.\\,prod\_a = (l.map(\\lambda f, f(a))).prod. $$$$

Lean4

@[to_additive]
theorem list_prod_apply {α : Type*} {M : α → Type*} [∀ a, Monoid (M a)] (a : α) (l : List (∀ a, M a)) :
    l.prod a = (l.map fun f : ∀ a, M a ↦ f a).prod :=
  map_list_prod (evalMonoidHom M a) _

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