coeComplex_mul

Mathlib.Analysis.Quaternion

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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