cast_natCast — Mathlib

English

Casting of natural numbers from ZMod n matches the natural cast: for k ∈ ℕ, (cast (k : ZMod n) : R) = k.

Русский

Приведение натурального числа из ZMod n совпадает с обычным приведением: (cast (k : ZMod n) : R) = k.

LaTeX

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

Lean4

@[simp, norm_cast]
theorem cast_natCast (h : m ∣ n) (k : ℕ) : (cast (k : ZMod n) : R) = k :=
  map_natCast (castHom h R) k

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