algebraMap_eq_ofReal

Mathlib.Analysis.RCLike.Basic

URI: https://scilib.ai/kg/mathlib#RCLike.algebraMap_eq_ofReal

English

The algebra map from ℝ to K equals the coe from Real to K.

Русский

Алгебраическая карта из ℝ в K равна вложению из Real в K.

LaTeX

$$$\operatorname{algebraMap}_{\mathbb{R},K} = \operatorname{ofReal}$$$

Lean4

theorem algebraMap_eq_ofReal : ⇑(algebraMap ℝ K) = ofReal :=
  rfl

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

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

Разделы

Аффилиация

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