abs_prod — Mathlib

English

For any finite set s and any function f, the absolute value of the product equals the product of the absolute values: |∏_{i∈s} f(i)| = ∏_{i∈s} |f(i)|.

Русский

Для любого конечного множества s и любой функции f выполняется |∏_{i∈s} f(i)| = ∏_{i∈s} |f(i)|.

LaTeX

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

Lean4

theorem abs_prod [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] (s : Finset ι) (f : ι → R) :
    |∏ x ∈ s, f x| = ∏ x ∈ s, |f x| :=
  map_prod absHom _ _

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