mod_eq_of_modEq

Mathlib.Data.Nat.ModEq

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

English

If a ≡ b (mod n) and b < n, then a mod n = b.

Русский

Если a ≡ b (mod n) и b < n, то a mod n = b.

LaTeX

$$$ a \equiv b [MOD n] \land b < n \Rightarrow a \bmod n = b $$$

Lean4

theorem mod_eq_of_modEq {a b n} (h : a ≡ b [MOD n]) (hb : b < n) : a % n = b :=
  Eq.trans h (mod_eq_of_lt hb)

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

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

Разделы

Аффилиация

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