normSq_div

Mathlib.Algebra.Quaternion

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

English

The norm is multiplicative with division: normSq(a / b) = normSq(a) / normSq(b).

Русский

Норма умножаема в делении: normSq(a / b) = normSq(a) / normSq(b).

LaTeX

$$$\operatorname{normSq}(a / b) = \operatorname{normSq}(a) / \operatorname{normSq}(b)$$$

Lean4

theorem normSq_div : normSq (a / b) = normSq a / normSq b :=
  map_div₀ normSq a b

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

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

Разделы

Аффилиация

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