norm_prod — Mathlib

English

For a list l of elements in α, the norm of the product of all elements equals the product of the norms of the elements.

Русский

Для списка элементов α норма произведения всех элементов равна произведению норм элементов.

LaTeX

$$$\\|\\prod\\, l\\| = (\\|\\cdot\\|)\\\\!_{l}.prod$$$

Lean4

protected theorem norm_prod (l : List α) : ‖l.prod‖ = (l.map norm).prod :=
  map_list_prod (normHom.toMonoidHom : α →* ℝ) _

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