natCast_modEq_natCast — Mathlib

English

For a, b, n ∈ ℕ, a ≡ b modulo n, interpreted via α, is equivalent to a ≡ b modulo n in the natural numbers.

Русский

Для a, b, n ∈ ℕ конгруэнтность a ≡ b по модулю n, рассматривая через α, эквивалентна a ≡ b по модулю n в ℕ.

LaTeX

$$$ a \equiv b \ [PMOD (n : \alpha)] \iff a \equiv b \ [MOD n] $$$

Lean4

@[simp, norm_cast]
theorem natCast_modEq_natCast {a b n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [MOD n] := by
  simp_rw [← Int.natCast_modEq_iff, ← modEq_iff_int_modEq, ← @intCast_modEq_intCast α, Int.cast_natCast]

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