normSq_nonneg

Mathlib.Algebra.Quaternion

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

English

normSq(a) is nonnegative: 0 ≤ normSq(a) for all quaternions a.

Русский

normSq(a) неотрицательна: 0 ≤ normSq(a) для любого a.

LaTeX

$$0 \leq \operatorname{normSq}(a)$$

Lean4

@[simp]
theorem normSq_nonneg : 0 ≤ normSq a := by
  rw [normSq_def']
  apply_rules [sq_nonneg, add_nonneg]

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

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

Разделы

Аффилиация

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