norm_div

Mathlib.Analysis.Normed.Field.Basic

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

English

The norm respects division: for a,b, ||a/b|| = ||a||/||b||.

Русский

Норма сохраняет деление: ||a/b|| = ||a|| / ||b||.

LaTeX

$$$\\|a/b\\| = \\|a\\| / \\|b\\|$$$

Lean4

@[simp]
theorem norm_div (a b : α) : ‖a / b‖ = ‖a‖ / ‖b‖ :=
  map_div₀ (normHom : α →*₀ ℝ) a b

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

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

Разделы

Аффилиация

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