intCast_mod — Mathlib

English

For any a ∈ ℤ and b ∈ ℕ, the reduction of a modulo b coincides with the ZMod representative.

Русский

Для любого a ∈ ℤ и b ∈ ℕ редукция a по модулю b совпадает с представителем в ZMod b.

LaTeX

$$$\forall a \in \mathbb{Z},\forall b \in \mathbb{N},\ ((a \bmod b : \mathbb{Z}) = (a : \mathbb{Z}) \bmod b)$$$

Lean4

@[push_cast, simp]
theorem intCast_mod (a : ℤ) (b : ℕ) : ((a % b : ℤ) : ZMod b) = (a : ZMod b) :=
  by
  rw [ZMod.intCast_eq_intCast_iff]
  apply Int.mod_modEq

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