one_def

Mathlib.GroupTheory.SpecificGroups.Quaternion

URI: https://scilib.ai/kg/mathlib#QuaternionGroup.one_def

English

In QuaternionGroup, the identity 1 equals a_0.

Русский

Единица 1 равна a_0.

LaTeX

$$$1 = a_0$$$

Lean4

theorem one_def : (1 : QuaternionGroup n) = a 0 :=
  rfl

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

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

Разделы

Аффилиация

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