coe_pow — Mathlib

English

The embedding preserves powers: for any real x and natural n, (x^n) embedded into EReal equals (x embedded) raised to the nth power.

Русский

Встраивание сохраняет степени: для любого x ∈ ℝ и натурального n, ↑(x^n) = (↑x)^n в EReal.

LaTeX

$$$ (\uparrow (x^n) : \mathrm{EReal}) = (\uparrow x : \mathrm{EReal})^n \quad (x \in \mathbb{R}, \ n \in \mathbb{N}) $$$

Lean4

@[simp, norm_cast]
theorem coe_pow (x : ℝ) (n : ℕ) : (↑(x ^ n) : EReal) = (x : EReal) ^ n :=
  map_pow (⟨⟨(↑), coe_one⟩, coe_mul⟩ : ℝ →* EReal) _ _

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