div_add_mod

Mathlib.Data.PNat.Basic

URI: https://scilib.ai/kg/mathlib#PNat.div_add_mod

English

For m,k ∈ ℕ⁺, mod m k + k × div m k = m.

Русский

Для m,k ∈ ℕ⁺, mod m k + k × div m k = m.

LaTeX

$$$$ \operatorname{mod}(m,k) + k \cdot \operatorname{div}(m,k) = m $$$$

Lean4

theorem div_add_mod (m k : ℕ+) : (k * div m k + mod m k : ℕ) = m :=
  (add_comm _ _).trans (mod_add_div _ _)

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

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

Разделы

Аффилиация

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