hurwitzEvenFEPair_zero_symm — Mathlib

English

The FE pair at a = 0 is symmetric: (hurwitzEvenFEPair 0).symm = hurwitzEvenFEPair 0.

Русский

Пара ФЕ при a = 0 симметрична: (hurwitzEvenFEPair 0).symm = hurwitzEvenFEPair 0.

LaTeX

$$$$ (\\mathrm{hurwitzEvenFEPair}(0)).\\mathrm{symm} = \\mathrm{hurwitzEvenFEPair}(0). $$$$

Lean4

@[simp]
theorem hurwitzEvenFEPair_zero_symm : (hurwitzEvenFEPair 0).symm = hurwitzEvenFEPair 0 :=
  by
  unfold hurwitzEvenFEPair WeakFEPair.symm
  congr 1 <;> simp [evenKernel_eq_cosKernel_of_zero]

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