zero_rpow

Mathlib.Analysis.SpecialFunctions.Pow.NNReal

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

English

For x ∈ ℝ, and x ≠ 0, 0^x = 0 in NNReal.

Русский

Для x ∈ ℝ и x ≠ 0, 0^x = 0 в NNReal.

LaTeX

$$$0^x = 0 \\quad( x \\neq 0 )$$$

Lean4

@[simp]
theorem zero_rpow {x : ℝ} (h : x ≠ 0) : (0 : ℝ≥0) ^ x = 0 :=
  NNReal.eq <| Real.zero_rpow h

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

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

Разделы

Аффилиация

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