eq_iff_modEq_nat — Mathlib

English

For natural numbers a,b, the equality (a : ZMod n) = b holds exactly when a ≡ b (mod n).

Русский

Для натуральных a,b равенство (a : ZMod n) = b происходит тогда и только тогда, когда a ≡ b (mod n).

LaTeX

$$$ (a : ZMod n) = b \iff a \equiv b [MOD n] $$$

Lean4

@[deprecated natCast_eq_natCast_iff (since := "2025-08-12")]
theorem eq_iff_modEq_nat (n : ℕ) {a b : ℕ} : (a : ZMod n) = b ↔ a ≡ b [MOD n] :=
  natCast_eq_natCast_iff a b n

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