instSubsingletonInfinitePlace

Mathlib.NumberTheory.NumberField.InfinitePlace.Basic

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

English

There is only one infinite place of the rational numbers, i.e., InfinitePlace(ℚ) is a Subsingleton.

Русский

УРациональных чисел существует единственное бесконечное место; т.е. InfinitePlace(ℚ) — подподборка.

LaTeX

$$Subsingleton (InfinitePlace \mathbb{Q})$$

Lean4

instance : Subsingleton (InfinitePlace ℚ) where allEq a b := by ext; simp

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

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

Разделы

Аффилиация

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