cast_sub — Mathlib

English

Casting preserves powers: (cast (a^k : ZMod n) : R) = (cast a)^k for k ∈ ℕ, under m | n.

Русский

Приведение сохраняет степени: cast(a^k) = (cast a)^k.

LaTeX

$$$\\\\forall {n : \\\\mathbb{N}} (a : ZMod n) (k : \\\\mathbb{N}) [CharP R m] (h : m \\\\mid n), \\\\operatorname{cast} (a^k) = (\\\\operatorname{cast} a)^k$$$

Lean4

@[simp]
theorem cast_sub (h : m ∣ n) (a b : ZMod n) : (cast (a - b : ZMod n) : R) = cast a - cast b :=
  (castHom h R).map_sub a b

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