rpow_ofNat

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#ENNReal.rpow_ofNat

English

For x ∈ ENNReal and n ∈ ℕ with n ≥ 2, x^((ofNat n) : ℝ) = x^(OfNat.ofNat n).

Русский

Для x ∈ ENNReal и n ∈ ℕ при n ≥ 2 верно x^{(ofNat(n) : ℝ)} = x^{(OfNat.ofNat n)}.

LaTeX

$$$ x^{(\mathrm{ofNat}(n) : \mathbb{R})} = x^{(\mathrm{OfNat.ofNat}\ n)} $$$

Lean4

@[simp]
theorem rpow_ofNat (x : ℝ≥0∞) (n : ℕ) [n.AtLeastTwo] : x ^ (ofNat(n) : ℝ) = x ^ (OfNat.ofNat n) :=
  rpow_natCast x n

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru