cast_pow — Mathlib

English

Casting preserves powers: (cast (a ^ k : ZMod n) : R) = (cast a) ^ k.

Русский

Приведение сохраняет степени: 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_pow (h : m ∣ n) (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a) ^ k :=
  (castHom h R).map_pow a k

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