mod_modEq

Mathlib.Data.Int.ModEq

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

English

Let a and n be integers. Then a mod n is congruent to a modulo n: a mod n ≡ a (mod n).

Русский

Пусть a и n — целые числа. Остаток a по модулю n удовлетворяет a mod n ≡ a (mod n).

LaTeX

$$$a \bmod n \equiv a \pmod n$$$

Lean4

theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
  emod_emod _ _

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

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

Разделы

Аффилиация

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