floorRing_ceil_eq

Mathlib.Algebra.Order.Floor.Defs

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

English

The ceiling function from FloorRing matches Int.ceil: FloorRing.ceil = Int.ceil.

Русский

Функция округления вверх FloorRing совпадает с Int.ceil: FloorRing.ceil = Int.ceil.

LaTeX

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

Lean4

@[simp]
theorem floorRing_ceil_eq : @FloorRing.ceil = @Int.ceil :=
  rfl

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

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

Разделы

Аффилиация

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