nnnorm_mul

Mathlib.Analysis.Normed.Ring.Basic

URI: https://scilib.ai/kg/mathlib#nnnorm_mul

English

In a normed ring with a multiplicative NNReal norm, the NNReal norm is multiplicative: ‖a b‖₊ = ‖a‖₊ ‖b‖₊.

Русский

Для нормы NNReal в нормированном кольце выполняется: ‖a b‖₊ = ‖a‖₊ ‖b‖₊.

LaTeX

$$$\\|a \\cdot b\\|_{+} = \\|a\\|_{+} \\cdot \\|b\\|_{+}$$$

Lean4

@[simp]
theorem nnnorm_mul : ‖a * b‖₊ = ‖a‖₊ * ‖b‖₊ :=
  NNReal.eq <| norm_mul a b

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru