imI_coeComplex

Mathlib.Analysis.Quaternion

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

English

For z ∈ ℂ, the i-component of its quaternion image equals z.im.

Русский

Для z ∈ ℂ компонент i изображения z в ℍ равна z.im.

LaTeX

$$$\\operatorname{Im}_i((z:\\mathbb{H})) = z_{\\mathrm{im}}.$$$

Lean4

@[simp, norm_cast]
theorem imI_coeComplex (z : ℂ) : (z : ℍ).imI = z.im :=
  rfl

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

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

Разделы

Аффилиация

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