emod_eq_sub_self_emod

Mathlib.Data.Int.DivMod

URI: https://scilib.ai/kg/mathlib#Int.emod_eq_sub_self_emod

English

For integers a,b, a mod b = (a − b) mod b.

Русский

Для целых чисел a, b выполняется a mod b = (a − b) mod b.

LaTeX

$$$a \% b = (a - b) \% b$$$

Lean4

theorem emod_eq_sub_self_emod {a b : Int} : a % b = (a - b) % b :=
  (sub_emod_right a b).symm

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

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

Разделы

Аффилиация

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