hurwitzEvenFEPair_neg — Mathlib

English

Replacing a by −a leaves the FE pair unchanged: hurwitzEvenFEPair(−a) = hurwitzEvenFEPair(a).

Русский

Замена a на −a не изменяет FE-пару: hurwitzEvenFEPair(−a) = hurwitzEvenFEPair(a).

LaTeX

$$$$ \\mathrm{hurwitzEvenFEPair}(-a) = \\mathrm{hurwitzEvenFEPair}(a). $$$$

Lean4

@[simp]
theorem hurwitzEvenFEPair_neg (a : UnitAddCircle) : hurwitzEvenFEPair (-a) = hurwitzEvenFEPair a :=
  by
  unfold hurwitzEvenFEPair
  congr 1 <;> simp [Function.comp_def]

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