ofReal_intCast

Mathlib.Analysis.RCLike.Basic

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

English

For every integer n, the image of n under the real embedding into K equals n in K.

Русский

Для каждого целого числа n образ через вещественное вложение в K равен n.

LaTeX

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

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_intCast (n : ℤ) : ((n : ℝ) : K) = n :=
  map_intCast _ n

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

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

Разделы

Аффилиация

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