cosKernel_neg

Mathlib.NumberTheory.LSeries.HurwitzZetaEven

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

← MathLib Explorer

English

A simplification lemma: cosKernel(-a) x = cosKernel a x.

Русский

Лемма упрощения: cosKernel(-a, x) = cosKernel(a, x).

LaTeX

$$$$\\cosKernel(-a, x) = \\cosKernel(a, x).$$$$

Lean4

@[simp]
theorem cosKernel_neg (a : UnitAddCircle) (x : ℝ) : cosKernel (-a) x = cosKernel a x := by
  induction a using QuotientAddGroup.induction_on with
  | H => simp [← QuotientAddGroup.mk_neg, ← ofReal_inj, cosKernel_def]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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