rpowIntegrand₀₁_zero_right

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

URI: https://scilib.ai/kg/mathlib#Real.rpowIntegrand₀₁_zero_right

English

The integrand vanishes when the second argument equals zero: rpowIntegrand₀₁ p t 0 = 0 for any p, t.

Русский

Интегранг равен нулю при втором аргументе равном нулю: rpowIntegrand₀₁ p t 0 = 0.

LaTeX

$$$rpowIntegrand_{01}(p,t,0) = 0$$$

Lean4

@[simp]
theorem rpowIntegrand₀₁_zero_right : rpowIntegrand₀₁ p t 0 = 0 := by simp [rpowIntegrand₀₁]

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

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

Разделы

Аффилиация

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