coe_pow — Mathlib

English

For r in ℝ≥0 and n a natural number, the Real-coercion of r^n equals r^n in Real: ((r^n : ℝ≥0) : ℝ) = (r : ℝ)^n.

Русский

Для r в ℝ≥0 и n ∈ ℕ, преобразование в Real от r^n равно r^n в Real: ((r^n : ℝ≥0) : ℝ) = (r : ℝ)^n.

LaTeX

$$$\big((r^n : \mathbb{R}_{\ge 0}) : \mathbb{R}\big) = (r : \mathbb{R})^{n}$$$

Lean4

@[simp, norm_cast]
theorem coe_pow (r : ℝ≥0) (n : ℕ) : ((r ^ n : ℝ≥0) : ℝ) = (r : ℝ) ^ n :=
  rfl

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