ofRealAm_coe

Mathlib.LinearAlgebra.Complex.Module

URI: https://scilib.ai/kg/mathlib#Complex.ofRealAm_coe

English

The real-to-complex algebra homomorphism is realized by the standard inclusion x ↦ x in ℂ.

Русский

Алгебра-гомоморфизм от ℝ в ℂ реализуется обычным включением x ↦ x в ℂ.

LaTeX

$$$\forall x\in\mathbb{R},\; \mathrm{ofRealAm}(x) = (x:\mathbb{C})$$$

Lean4

@[simp]
theorem ofRealAm_coe : ⇑ofRealAm = ((↑) : ℝ → ℂ) :=
  rfl

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

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

Разделы

Аффилиация

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