evenKernel_eq_cosKernel_of_zero — Mathlib

English

For a ∈ UnitAddCircle, at a = 0 the even kernel equals the cosine kernel.

Русский

Для a ∈ UnitAddCircle при a = 0 четное ядро равно косинусному ядру.

LaTeX

$$$$\\text{EvenKernel}(0) = \\text{CosKernel}(0).$$$$

Lean4

/-- For `a = 0`, both kernels agree. -/
theorem evenKernel_eq_cosKernel_of_zero : evenKernel 0 = cosKernel 0 :=
  by
  ext1 x
  simp [← QuotientAddGroup.mk_zero, ← ofReal_inj, evenKernel_def, cosKernel_def]

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