zero_nnrpow

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic

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

English

If a = a' and y = y', then nnrpow a y = nnrpow a' y'.

Русский

Если a = a' и y = y', то nnrpow a y = nnrpow a' y'.

LaTeX

$$a = a' → y = y' → nnrpow a y = nnrpow a' y'$$

Lean4

@[simp]
theorem zero_nnrpow {x : ℝ≥0} : (0 : A) ^ x = 0 := by simp [nnrpow_def]

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

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

Разделы

Аффилиация

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