rpow_zero

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

URI: https://scilib.ai/kg/mathlib#NNReal.rpow_zero

English

For x ∈ NNReal, x^0 = 1 (as a NNReal).

Русский

Для x ∈ ℝ≥0 верно x^0 = 1 (в NNReal).

LaTeX

$$$\\displaystyle x^0 = 1$$$

Lean4

@[simp]
theorem rpow_zero (x : ℝ≥0) : x ^ (0 : ℝ) = 1 :=
  NNReal.eq <| Real.rpow_zero _

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

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

Разделы

Аффилиация

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