mk_prod — Mathlib

English

Finite products of mk distribute: product over t of mk(f i) (s i) equals mk(product f i, product s i).

Русский

Произведение конечного числа mk распределяется: произведение по i∈t mk(f i)(s i) равно mk(∏ f i, ∏ s i).

LaTeX

$$$ \prod_{i\in t} mk\left(f(i),s(i)\right) = mk\left(\prod_{i\in t} f(i), \prod_{i\in t} s(i)\right) $$$

Lean4

@[to_additive]
theorem mk_prod {ι} (t : Finset ι) (f : ι → M) (s : ι → S) :
    ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i) := by
  classical induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]

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