ofReal_zpow — Mathlib

English

For any real r and integer n, the real power and zpow embedding commute: ((r^n : ℝ) : K) = (r : K)^n.

Русский

Для любого r ∈ ℝ и целого n, вещевая степень и zpow‑поле совместимы: ((r^n : ℝ) : K) = (r : K)^n.

LaTeX

$$$$ ((r^n : \mathbb{R}) : K) = (r : K)^n. $$$$

Lean4

@[rclike_simps, norm_cast]
theorem ofReal_zpow (r : ℝ) (n : ℤ) : ((r ^ n : ℝ) : K) = (r : K) ^ n :=
  map_zpow₀ (algebraMap ℝ K) r n

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