floorRing_floor_eq

Mathlib.Algebra.Order.Floor.Defs

URI: https://scilib.ai/kg/mathlib#Int.floorRing_floor_eq

English

The floor function defined via FloorRing is the same as the standard Int.floor function: FloorRing.floor = Int.floor.

Русский

Функция округления вниз, заданная через FloorRing, совпадает с обычной функцией Int.floor: FloorRing.floor = Int.floor.

LaTeX

$$$\text{FloorRing.floor} = \text{Int.floor}.$$$

Lean4

@[simp]
theorem floorRing_floor_eq : @FloorRing.floor = @Int.floor :=
  rfl

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

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

Разделы

Аффилиация

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