instIsStarNormal

Mathlib.Algebra.Quaternion

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

English

For every a in ℍ(R), a is a StarNormal element; i.e., IsStarNormal a holds.

Русский

Для каждого элемента a ∈ ℍ(R) выполняется IsStarNormal a.

LaTeX

$$$$ \forall a \in \mathbb{H}(R), \ \text{IsStarNormal}(a). $$$$

Lean4

instance : IsStarNormal a :=
  inferInstanceAs <| IsStarNormal (R := ℍ[R,-1,0,-1]) a

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

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

Разделы

Аффилиация

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