Theorems · Theorem · number theory

ModularForm.trace.congr_simp

∀ {𝒢 𝒢_1 : Subgroup (GL (Fin 2) ℝ)} (e_𝒢 : 𝒢 = 𝒢_1) (ℋ : Subgroup (GL (Fin 2) ℝ)) {F : Type u_1} (f f_1 : F),
  f = f_1 →
    ∀ [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [inst_1 : 𝒢.IsFiniteRelIndex ℋ] [inst_2 : ModularFormClass F 𝒢 k],
      ModularForm.trace ℋ f = ModularForm.trace ℋ f_1

Defined in

Mathlib.NumberTheory.ModularForms.NormTrace

Cited by

0 results in Mathlib

Foundations

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

Assumes

FunLikeSubgroup.IsFiniteRelIndexModularFormClass