eq_of_mod_eq_of_natAbs_sub_lt_natAbs

English

If a ≡ c (mod b) and natAbs(a − c) < natAbs(b), then a = c.

Русский

Если a ≡ c (mod b) и natAbs(a − c) < natAbs(b), тогда a = c.

LaTeX

$$$a \\equiv c \\pmod{b} \\quad \\land \\; |a-c|_{\\mathbb{Z}} < |b|_{\\mathbb{Z}} \\;\Rightarrow\\; a=c$$$

Lean4

/-- If two integers are congruent to a sufficiently large modulus, they are equal. -/
theorem eq_of_mod_eq_of_natAbs_sub_lt_natAbs {a b c : ℤ} (h1 : a % b = c) (h2 : natAbs (a - c) < natAbs b) : a = c :=
  Int.eq_of_sub_eq_zero (eq_zero_of_dvd_of_natAbs_lt_natAbs (dvd_self_sub_of_emod_eq h1) h2)

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