ofReal_zpow — Mathlib

English

For real r and integer n, the embedding commutes with integer powers: ofReal(r^n) = (ofReal(r))^n.

Русский

Для вещественного r и целого n отражение сохраняет целочисленные степени: ofReal(r^n) = (ofReal(r))^n.

LaTeX

$$$$\operatorname{ofReal}(r^{n}) = (\operatorname{ofReal}(r))^{n}.$$$$

Lean4

@[simp, norm_cast]
theorem ofReal_zpow (r : ℝ) (n : ℤ) : ((r ^ n : ℝ) : ℂ) = (r : ℂ) ^ n :=
  map_zpow₀ ofRealHom r n

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