oddKernel_zero

Mathlib.NumberTheory.LSeries.HurwitzZetaOdd

URI: https://scilib.ai/kg/mathlib#HurwitzZeta.oddKernel_zero

English

The odd kernel evaluated at a = 0 is identically zero: oddKernel 0 x = 0 for all x.

Русский

Нечетное ядро при a=0 равно нулю: oddKernel 0 x = 0 для всех x.

LaTeX

$$$$\\text{oddKernel}(0,x) = 0.$$$$

Lean4

@[simp]
theorem oddKernel_zero (x : ℝ) : oddKernel 0 x = 0 := by simpa using oddKernel_neg 0 x

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

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

Разделы

Аффилиация

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