coe_prod — Mathlib

English

Let f: ι → positive naturals. Then the natural-coercion of the product equals the product of the coerced factors: ↑(∏ i∈s, f(i)) = ∏ i∈s, f(i) in ℕ.

Русский

Пусть f: ι → ℕ⁺. Тогда привести произведение к ℕ через натуральное включение соответствует произведению самих приводимых членов: ↑(∏ i∈s, f(i)) = ∏ i∈s, f(i).

LaTeX

$$$\uparrow\left(\prod_{i \in s} f(i)\right) = \prod_{i \in s} (f(i)\; : \; \mathbb{N})$$$

Lean4

@[simp, norm_cast]
theorem coe_prod {ι : Type*} (f : ι → ℕ+) (s : Finset ι) : ↑(∏ i ∈ s, f i) = (∏ i ∈ s, f i : ℕ) :=
  map_prod PNat.coeMonoidHom _ _

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