div_add_mod'

Mathlib.Data.PNat.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

theorem div_add_mod' (m k : ℕ+) : (div m k * k + mod m k : ℕ) = m :=
  by
  rw [mul_comm]
  exact div_add_mod _ _

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

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

Разделы

Аффилиация

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