sub_floor_div_mul_nonneg

Mathlib.Algebra.Order.Floor.Ring

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

English

For any a,b with b > 0, a − floor(a/b)·b ≥ 0.

Русский

Пусть b > 0; тогда a − ⌊a/b⌋·b ≥ 0.

LaTeX

$$$0 \\\\le a - \\\\lfloor a/b \\\\rfloor \\\\cdot b$$$

Lean4

theorem sub_floor_div_mul_nonneg (a : k) (hb : 0 < b) : 0 ≤ a - ⌊a / b⌋ * b :=
  sub_nonneg_of_le <| (le_div_iff₀ hb).1 <| floor_le _

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

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

Разделы

Аффилиация

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