intCast_cast_sub — Mathlib

English

For x,y ∈ ZMod n, the integer cast of x−y equals (cast x − cast y) mod n.

Русский

Для x, y ∈ ZMod n целочисленное представление разности x−y равно (cast x − cast y) mod n.

LaTeX

$$$\forall x,y \in \mathbb{Z}/n\mathbb{Z},\ (\operatorname{cast}(x - y) : \mathbb{Z}) = (\operatorname{cast}(x) - \operatorname{cast}(y)) \bmod n$$$

Lean4

theorem intCast_cast_sub (x y : ZMod n) : (cast (x - y) : ℤ) = (cast x - cast y) % n := by
  rw [← ZMod.coe_intCast, Int.cast_sub, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

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