mod_modEq

Mathlib.Data.Nat.ModEq

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

English

a mod n ≡ a (mod n).

Русский

a по модулю n эквивалентно a по модулю n.

LaTeX

$$$a \\bmod n \\equiv a \\pmod{n}$$$

Lean4

theorem mod_modEq (a n) : a % n ≡ a [MOD n] :=
  mod_mod _ _

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

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

Разделы

Аффилиация

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