isReal_infinitePlace

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

URI: https://scilib.ai/kg/mathlib#Rat.isReal_infinitePlace

English

The infinite place of the rationals is real; i.e., IsReal(infinitePlace) holds for Rat.

Русский

Бесконечное место рациональных чисел является реальным; т.е. IsReal(infinitePlace) верно.

LaTeX

$$IsReal (infinitePlace) for Rat$$

Lean4

theorem isReal_infinitePlace : InfinitePlace.IsReal (infinitePlace) :=
  ⟨Rat.castHom ℂ, by ext; simp, rfl⟩

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

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

Разделы

Аффилиация

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