nnnorm_div — Mathlib

English

For a normed division ring α and elements a,b ∈ α, the nonnegative norm respects division: ‖a/b‖₊ = ‖a‖₊ / ‖b‖₊.

Русский

Для нормированного делимого кольца α и элементов a, b ∈ α справедливо: ‖a/b‖₊ = ‖a‖₊ / ‖b‖₊.

LaTeX

$$$\|a/b\|_+ = \|a\|_+/\|b\|_+.$$$

Lean4

@[simp]
theorem nnnorm_div (a b : α) : ‖a / b‖₊ = ‖a‖₊ / ‖b‖₊ :=
  map_div₀ (nnnormHom : α →*₀ ℝ≥0) a b

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