nnnorm_coe

Mathlib.Analysis.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.nnnorm_coe

English

The nonnegative norm agrees on real scalars: ∥(a : ℍ)∥₊ = ∥a∥₊ for all a ∈ ℝ.

Русский

Нормa nn совпадает на вещественных скалярах: ∥(a : ℍ)∥₊ = ∥a∥₊ для всех a ∈ ℝ.

LaTeX

$$$\\| (a : \\mathbb{H}) \\|_+ = \\| a \\|_+ \\quad (a \\in \\mathbb{R}).$$$

Lean4

@[simp, norm_cast]
theorem nnnorm_coe (a : ℝ) : ‖(a : ℍ)‖₊ = ‖a‖₊ :=
  Subtype.ext <| norm_coe a

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

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

Разделы

Аффилиация

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