map_prod — Mathlib

English

Under an absolute value abv, the product maps to the product of the values: abv(∏ f i) = ∏ abv(f i).

Русский

При абс. значении abv произведение переходит в произведение значений: 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

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

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