ofReal_ratCast

Mathlib.Analysis.RCLike.Basic

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

English

For any rational q, the real embedding of q into K equals q in K.

Русский

Для любого рационального числа q образ через вещественное вложение в K равен q.

LaTeX

$$$$((q : \mathbb{R}) : K) = q.$$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_ratCast (n : ℚ) : ((n : ℝ) : K) = n :=
  map_ratCast _ n

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

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

Разделы

Аффилиация

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