intCast_cast_add — Mathlib

English

For elements x,y in ZMod n, the integer cast of x+y equals the remainder of the sum of the casts: cast(x+y) = (cast x + cast y) mod n.

Русский

Для элементов x, y в ZMod n целочисленное представление суммы x+y равно остатку от суммы представлений: cast(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_add (x y : ZMod n) : (cast (x + y) : ℤ) = (cast x + cast y) % n := by
  rw [← ZMod.coe_intCast, Int.cast_add, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

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