intCast_cast_mul — Mathlib

English

For x,y in 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 \cdot y) : \mathbb{Z}) = (\operatorname{cast}(x) \cdot \operatorname{cast}(y)) \bmod n$$$

Lean4

theorem intCast_cast_mul (x y : ZMod n) : (cast (x * y) : ℤ) = cast x * cast y % n := by
  rw [← ZMod.coe_intCast, Int.cast_mul, ZMod.intCast_zmod_cast, ZMod.intCast_zmod_cast]

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