zero_rpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

Rpow of zero with nonzero exponent equals zero.

Русский

rpow(0, x) = 0 при x ≠ 0.

LaTeX

$${x ≠ 0} ⇒ rpow(0, x) = 0$$

Lean4

theorem zero_rpow {x : ℝ} (hx : x ≠ 0) : rpow (0 : A) x = 0 := by simp [rpow, NNReal.zero_rpow hx]

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

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

Разделы

Аффилиация

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