cast_zpow — Mathlib

English

For α a DivisionRing of characteristic zero and p ∈ ℚ, n ∈ ℤ, the cast to α commutes with integer powers: (p^n)↑ = (p^n)↑.

Русский

Для α делимого кольца характеристика ноль и p ∈ ℚ, n ∈ ℤ, приведение сохраняет возведение в степени целого числа: ↑(p^n) = (p^n)↑.

LaTeX

$$$ \uparrow(p^{n}) = (p^{n})^{\uparrow} $$$

Lean4

@[simp, norm_cast]
theorem cast_zpow (p : ℚ) (n : ℤ) : ↑(p ^ n) = (p ^ n : α) :=
  map_zpow₀ (castHom α) ..

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