dist_mul_left

Mathlib.Data.Nat.Dist

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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