cast_prod — Mathlib

English

Let s be a finite collection of indices and f a function from the index set to nonnegative rational numbers. The embedding of nonnegative rationals into a semifield preserves products over s: the image of the product equals the product of the images.

Русский

Пусть s — конечное семейство индексов, f: α → ℚ≥0. Приведение NN Rat в полевой сохраняет произведение: образ произведения равен произведению образов.

LaTeX

$$$((\prod_{a \in s} f(a)) : K) = \prod_{a \in s} (f(a) : K)$$$

Lean4

@[norm_cast]
theorem cast_prod (s : Finset α) (f : α → ℚ≥0) : ↑(∏ a ∈ s, f a) = ∏ a ∈ s, (f a : K) :=
  map_prod (castHom _) _ _

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