mod_add_div'

Mathlib.Data.PNat.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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