cast_intCast — Mathlib

English

Casting from integers via ZMod recovers the integer: for h, (cast (k : ZMod n) : R) = k for k ∈ ℤ.

Русский

Приведение через ZMod восстанавливает целое число: (cast (k : ZMod n) : R) = k.

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} {R : Type*} [Ring R] (h : m \\\\mid n) (k : \\\\mathbb{Z}), \\\\operatorname{cast} (k : ZMod n) = k$$$

Lean4

@[simp, norm_cast]
theorem cast_intCast (h : m ∣ n) (k : ℤ) : (cast (k : ZMod n) : R) = k :=
  map_intCast (castHom h R) k

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