coeComplex_add

Mathlib.Analysis.Quaternion

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

English

The embedding from ℂ to ℍ preserves addition: ↑(z + w) = ↑z + ↑w for all z,w ∈ ℂ.

Русский

Вложение ℂ в ℍ сохраняет сложение: ↑(z + w) = ↑z + ↑w для всех z,w ∈ ℂ.

LaTeX

$$$\\uparrow(z+w) = \\uparrow z + \\uparrow w \\quad (z,w \\in \\mathbb{C}).$$$

Lean4

@[simp, norm_cast]
theorem coeComplex_add (z w : ℂ) : ↑(z + w) = (z + w : ℍ) := by ext <;> simp

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

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

Разделы

Аффилиация

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