cast_pow' — Mathlib

English

Let n be a natural number and R a ring of characteristic n. For every a in ZMod n and every k in N, the image of a^k under the canonical map to R equals the k-th power of the image of a in R.

Русский

Пусть n — натуральное число, R — кольцо характеристикой n. Для любого a ∈ ZMod n и любого k ∈ ℕ выполняется: образ a^k в R через каноническое отображение равен (образ a в R)^k.

LaTeX

$$$ (cast (a ^ k : ZMod n) : R) = (cast a : R) ^ k $$$

Lean4

theorem cast_pow' (a : ZMod n) (k : ℕ) : (cast (a ^ k : ZMod n) : R) = (cast a : R) ^ k := by simp

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