selfZPow_natCast — Mathlib

English

For natural exponents d, selfZPow x B d matches the usual image x^d in the localization.

Русский

Для натуральных показателей d элемент selfZPow x B d совпадает с обычной степенью x^d в локализации.

LaTeX

$$$selfZPow\!\_\! x B d = (algebraMap\ R\ B\ x)^d$$$

Lean4

@[simp]
theorem selfZPow_natCast (d : ℕ) : selfZPow x B d = algebraMap R B x ^ d :=
  selfZPow_of_nonneg _ _ (Int.natCast_nonneg d)

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