add_div_eq_of_le_mod_add_mod

Mathlib.Data.Nat.ModEq

URI: https://scilib.ai/kg/mathlib#Nat.add_div_eq_of_le_mod_add_mod

← MathLib Explorer

English

If a % c + b % c < c, then (a+b)/c = a/c + b/c.

Русский

Если a%c + b%c < c, то (a+b)/c = a/c + b/c.

LaTeX

$$$\\\\forall a,b,c \\\\in \\\\mathbb{N},\\\\ a \\\\bmod c + b \\\\bmod c < c \\\\Rightarrow (\\\\a+b)/c = a/c + b/c$$$

Lean4

theorem add_div_eq_of_le_mod_add_mod {a b c : ℕ} (hc : c ≤ a % c + b % c) (hc0 : 0 < c) :
    (a + b) / c = a / c + b / c + 1 := by rw [Nat.add_div hc0, if_pos hc]

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

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

Разделы

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

Аффилиация

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