re_coeComplex

Mathlib.Analysis.Quaternion

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

English

For any z ∈ ℂ, the real part of its image in ℍ equals z.re.

Русский

Для любого z ∈ ℂ действительная часть изображения z в ℍ равна z.re.

LaTeX

$$$\\operatorname{Re}((z:\\mathbb{H})) = z_{\\mathrm{re}}.$$

Lean4

@[simp, norm_cast]
theorem re_coeComplex (z : ℂ) : (z : ℍ).re = z.re :=
  rfl

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

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

Разделы

Аффилиация

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