instFloorRing

Mathlib.Data.Rat.Floor

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

English

The rational numbers carry a floor operation making them a FloorRing.

Русский

Рациональные числа образуют структуру FloorRing с операцией floor.

LaTeX

$$ℚ is a FloorRing$$

Lean4

instance : FloorRing ℚ :=
  (FloorRing.ofFloor ℚ Rat.floor) fun _ _ => Rat.le_floor_iff.symm

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

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

Разделы

Аффилиация

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