smul_ceilDiv

Mathlib.Algebra.Order.Floor.Div

URI: https://scilib.ai/kg/mathlib#smul_ceilDiv

← MathLib Explorer

English

For all a, floorDiv by a is at most ceilDiv by a.

Русский

Для всех a величина floorDiv по a не больше ceilDiv по a.

LaTeX

$$$ \\forall a, \\\\ floorDiv(b,a) \\\\le ceilDiv(b,a).$$$

Lean4

@[simp]
theorem smul_ceilDiv [PosSMulMono α β] [PosSMulReflectLE α β] (ha : 0 < a) (b : β) : a • b ⌈/⌉ a = b :=
  eq_of_forall_ge_iff <| by simp [smul_le_smul_iff_of_pos_left, ha]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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