coe_prod — Mathlib

English

The germ of a finite product function equals the product of the germs.

Русский

Герм функции-образа продукта в конечном количестве переменных равен произведению гемов функций.

LaTeX

$$$\mathrm{Germ}^l\left(\prod_{i \in s} f_i\right) = \prod_{i \in s} \mathrm{Germ}^l(f_i).$$$

Lean4

@[to_additive (attr := simp)]
theorem coe_prod {α : Type*} (l : Filter α) (R : Type*) [CommMonoid R] {ι} (f : ι → α → R) (s : Finset ι) :
    ((∏ i ∈ s, f i : α → R) : Germ l R) = ∏ i ∈ s, (f i : Germ l R) :=
  map_prod (Germ.coeMulHom l : (α → R) →* Germ l R) f s

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