coe_one

Mathlib.Algebra.Quaternion

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

English

The embedding of 1 from R into the quaternion algebra is the quaternion 1.

Русский

Встроение единицы из R в ℍ[R] равно единице в ℍ[R].

LaTeX

$$$$\iota(1) = 1.$$$$

Lean4

@[simp, norm_cast]
theorem coe_one : ((1 : R) : ℍ[R]) = 1 :=
  rfl

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

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

Разделы

Аффилиация

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