dist_eq'

Mathlib.Topology.Instances.Int

URI: https://scilib.ai/kg/mathlib#Int.dist_eq'

English

A variant: dist m n equals the absolute value of m−n in integers, with casts consistent.

Русский

Вариант: dist m n равно модулю m−n в целых, совместимо с приведением типов.

LaTeX

$$$\\mathrm{dist}(m,n) = |m - n|$ для m,n ∈ \\mathbb{Z}$$$

Lean4

theorem dist_eq' (m n : ℤ) : dist m n = |m - n| := by rw [dist_eq]; norm_cast

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

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

Разделы

Аффилиация

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