eq

Mathlib.Data.Int.ModEq

URI: https://scilib.ai/kg/mathlib#Int.ModEq.eq

English

If a ≡ b mod n, then a ≡ b [ZMOD n] implies a % n = b % n.

Русский

Если a эквивалентно b по модулю n, то a ≡ b [ZMOD n] эквивалентно a % n = b % n.

LaTeX

$$$ a \equiv b \,[ZMOD n] \Rightarrow a \% n = b \% n $$$

Lean4

protected theorem eq : a ≡ b [ZMOD n] → a % n = b % n :=
  id

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

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

Разделы

Аффилиация

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