coe_algebraMap

Mathlib.LinearAlgebra.Complex.Module

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

English

The real-algebra embedding into ℂ coincides with the standard real coercion.

Русский

Встроение вещественных чисел в ℂ совпадает с обычной вложенностью вещественных чисел.

LaTeX

$$$\\\\operatorname{coe}_{\\\\mathbb{R} \\\\to \\\\mathbb{C}} = \\\\text{(coe)}$$$

Lean4

@[simp]
theorem coe_algebraMap : (algebraMap ℝ ℂ : ℝ → ℂ) = ((↑) : ℝ → ℂ) :=
  rfl

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

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

Разделы

Аффилиация

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