natCast_modEq_iff — Mathlib

English

For natural numbers a,b,n, a ≡ b [ZMOD n] is equivalent to a ≡ b [MOD n] after natural casting.

Русский

Для натуральных a,b,n: a ≡ b [ZMOD n] эквивалентно a ≡ b [MOD n] после приведения к натуралу.

LaTeX

$$$ \forall {a b n: \mathbb{N}}, a \equiv b \,[ZMOD n] \iff a \equiv b \,[MOD n] $$$

Lean4

@[simp, norm_cast]
theorem natCast_modEq_iff {a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] := by unfold ModEq Nat.ModEq;
  rw [← Int.ofNat_inj]; simp

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