map_prod — Mathlib

English

The absolute value of a finite product is the product of the absolute values of the factors, i.e., abv(∏ f i) = ∏ abv(f i).

Русский

Модуль произведения равен произведению модулей факторов: abv(∏ f_i) = ∏ abv(f_i).

LaTeX

$$$\operatorname{abv}\left(\prod_{i\in s} f(i)\right) = \prod_{i\in s} \operatorname{abv}(f(i))$$$

Lean4

nonrec theorem map_prod [CommSemiring R] [Nontrivial R] [CommRing S] [LinearOrder S] [IsStrictOrderedRing S]
    (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι) : abv (∏ i ∈ s, f i) = ∏ i ∈ s, abv (f i) :=
  map_prod abv f s

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