prod_hom_nonempty — Mathlib

English

If l is a nonempty list and f is a monoid hom, then (l.map f).prod = f(l.prod).

Русский

Если список непустой и f — гомоморфизм моноидов, то произведение отображённых элементов равно отображённому произведению исходного списка.

LaTeX

$$$$\\text{If } l \\neq ∅,\\; (l.map\\ f).prod = f(l.prod). $$$$

Lean4

@[to_additive]
theorem prod_hom_nonempty {l : List M} {F : Type*} [FunLike F M N] [MulHomClass F M N] (f : F) (hl : l ≠ []) :
    (l.map f).prod = f l.prod :=
  match l, hl with
  | x :: xs, hl => by induction xs generalizing x <;> simp_all

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