dist_mul_right

Mathlib.Data.Nat.Dist

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

English

For all n,m,k ∈ ℕ, dist(n·k, m·k) = dist(n,m)·k.

Русский

Для любых n,m,k ∈ ℕ верно: dist(n·k, m·k) = dist(n,m)·k.

LaTeX

$$$$ dist(n\cdot k, m\cdot k) = dist(n,m) \cdot k. $$$$

Lean4

theorem dist_mul_right (n k m : ℕ) : dist (n * k) (m * k) = dist n m * k := by
  rw [dist, dist, right_distrib, tsub_mul n, tsub_mul m]

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

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

Разделы

Аффилиация

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