modEq_iff_dvd'

Mathlib.Data.Nat.ModEq

URI: https://scilib.ai/kg/mathlib#Nat.modEq_iff_dvd'

← MathLib Explorer

English

If a ≤ b, then a ≡ b (mod n) iff n ∣ b − a.

Русский

Если a ≤ b, то a ≡ b (mod n) эквивалентно n делит b − a.

LaTeX

$$$a \le b \Rightarrow a \\equiv b \\pmod{n} \\iff n \\mid (b - a)$$$

Lean4

/-- A variant of `modEq_iff_dvd` with `Nat` divisibility -/
theorem modEq_iff_dvd' (h : a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a := by
  rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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