ofReal_alg

Mathlib.Analysis.RCLike.Basic

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

English

For every real x, ofReal x equals x times the unit in K.

Русский

Для каждого действительного x, ofReal x равно x умножить на единицу в K.

LaTeX

$$$\operatorname{ofReal}(x) = x \cdot 1_K$$$

Lean4

theorem ofReal_alg (x : ℝ) : (x : K) = x • (1 : K) :=
  Algebra.algebraMap_eq_smul_one x

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

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

Разделы

Аффилиация

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