instIsDomain

Mathlib.Algebra.Quaternion

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

English

For any quaternion a, (a.im)^2 = -normSq(a.im).

Русский

Для любого квартониона a: (a.im)^2 = -normSq(a.im).

LaTeX

$$(a.im)^2 = -\operatorname{normSq}(a.im)$$

Lean4

instance : IsDomain ℍ[R] :=
  NoZeroDivisors.to_isDomain _

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

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

Разделы

Аффилиация

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