reLm_coe

Mathlib.LinearAlgebra.Complex.Module

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

English

The real-part linear map coincides with the standard real-part function on ℂ.

Русский

Линеарная карта вещественной части совпадает с обычной функцией вещественной части на ℂ.

LaTeX

$$$ \mathrm{reLm}(z) = \mathrm{Re}(z) \quad \text{for all } z \in \mathbb{C}. $$$

Lean4

@[simp]
theorem reLm_coe : ⇑reLm = re :=
  rfl

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

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

Разделы

Аффилиация

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