norm_mul_le

Mathlib.Analysis.Normed.Ring.Basic

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

English

In a nonunital seminormed ring, the norm is submultiplicative: ‖a b‖ ≤ ‖a‖ ‖b‖.

Русский

В неединичном полугруппе с нормой норма умножения подмножество: \|ab\| ≤ \|a\|\|b\|.

LaTeX

$$$\|a b\| \leq \|a\| \|b\|$$$

Lean4

/-- The norm is submultiplicative. -/
theorem norm_mul_le (a b : α) : ‖a * b‖ ≤ ‖a‖ * ‖b‖ :=
  NonUnitalSeminormedRing.norm_mul_le a b

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

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

Разделы

Аффилиация

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