Theorems · Theorem · number theory

SlashInvariantForm.quotientFunc.congr_simp

∀ {𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)} {F : Type u_1} (f f_1 : F),
  f = f_1 →
    ∀ [inst : FunLike F UpperHalfPlane ℂ] {k k_1 : ℤ} (e_k : k = k_1) [inst_1 : SlashInvariantFormClass F 𝒢 k]
      (q q_1 : ↥ℋ ⧸ 𝒢.subgroupOf ℋ),
      q = q_1 →
        ∀ (τ τ_1 : UpperHalfPlane),
          τ = τ_1 → SlashInvariantForm.quotientFunc f q τ = SlashInvariantForm.quotientFunc f_1 q_1 τ_1

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

0 results in Mathlib

Foundations

Depth 179 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FunLikeSlashInvariantFormClass