norm_mul

Mathlib.Analysis.Normed.Ring.Basic

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

English

In any normed ring, the norm is multiplicative over multiplication: ‖a b‖ = ‖a‖ ‖b‖.

Русский

В нормированном кольце норма мультипликативна: ‖a b‖ = ‖a‖ ‖b‖.

LaTeX

$$$\\|a\\cdot b\\| = \\|a\\|\\cdot \\|b\\|$$$

Lean4

@[simp]
theorem norm_mul [Norm α] [Mul α] [NormMulClass α] (a b : α) : ‖a * b‖ = ‖a‖ * ‖b‖ :=
  NormMulClass.norm_mul a b

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

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

Разделы

Аффилиация

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