modEq_iff_int_modEq — Mathlib

English

A ≡ B (mod z) for integers is equivalent to A ≡ B (mod z) in the integer-modulus sense.

Русский

A ≡ B (mod z) для целых чисел эквивалентно A ≡ B (mod z) в смысле целочисленного модуля.

LaTeX

$$$ a \\equiv b \\pmod{z} \\iff a \\equiv b \\pmod{z} $$$

Lean4

@[simp]
theorem modEq_iff_int_modEq {a b z : ℤ} : a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z] := by
  simp [ModEq, dvd_iff_exists_eq_mul_left, Int.modEq_iff_dvd]

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