eisensteinSeries_SIF_apply — Mathlib

English

The evaluation of the SlashInvariantForm EisensteinSeries_SIF at a point coincides with the evaluation of the underlying EisensteinSeries function.

Русский

Значение SlashInvariantForm EisensteinSeries_SIF в точке совпадает с значением исходной функции EisensteinSeries.

LaTeX

$$$\mathrm{eisensteinSeries\_SIF}\_{{a}}(k,z) = \mathrm{eisensteinSeries}\_{{a}}(k,z).$$$

Lean4

theorem eisensteinSeries_SIF_apply (k : ℤ) (z : ℍ) : eisensteinSeries_SIF a k z = eisensteinSeries a k z :=
  rfl

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