Theorems · Theorem · number theory

EisensteinSeries.eisSummand_SL2_apply

∀ (k : ℤ) (i : Fin 2 → ℤ) (A : Matrix.SpecialLinearGroup (Fin 2) ℤ) (z : UpperHalfPlane),
  EisensteinSeries.eisSummand k i (A • z) =
    UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) A)) ↑z ^
        k *
      EisensteinSeries.eisSummand k (Matrix.vecMul i ↑A) z

How the eisSummand function changes under the Moebius action.

Defined in: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
Cited by: 1 results in Mathlib
Foundations: Depth 176 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites35

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement and proof · cited by 62,936
Realstatement and proof · cited by 25,697
Complexstatement and proof · cited by 5,565
Matrixstatement · cited by 4,303
mul_oneproof · cited by 3,885
MonoidHomstatement · cited by 3,629
one_mulproof · cited by 2,841
add_zeroproof · cited by 2,707
Units.valproof · cited by 1,966
Complex.ofRealproof · cited by 1,654
pow_oneproof · cited by 894
one_ne_zeroproof · cited by 885

Cited by1

Results whose statement or proof uses this declaration.

EisensteinSeries.eisensteinSeries_slash_applyproof · cited by 1