intCast_modEq_intCast' — Mathlib

English

Let a, b be integers and n a natural. The congruence a ≡ b modulo n, viewed via α, is equivalent to a ≡ b modulo n in ℤ.

Русский

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

LaTeX

$$$ a \equiv b \ [PMOD (n : \alpha)] \iff a \equiv b \ [PMOD (n : \mathbb{Z})] $$$

Lean4

@[simp, norm_cast]
theorem intCast_modEq_intCast' {a b : ℤ} {n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [PMOD (n : ℤ)] := by
  simpa using intCast_modEq_intCast (α := α) (z := n)

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