Theorems · Theorem · number theory

ModularForm.mk.inj

∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {toSlashInvariantForm : SlashInvariantForm Γ k}
  {holo' : MDiff ⇑toSlashInvariantForm}
  {bdd_at_cusps' : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm.toFun k}
  {toSlashInvariantForm_1 : SlashInvariantForm Γ k} {holo'_1 : MDiff ⇑toSlashInvariantForm_1}
  {bdd_at_cusps'_1 : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm_1.toFun k},
  { toSlashInvariantForm := toSlashInvariantForm, holo' := holo', bdd_at_cusps' := bdd_at_cusps' } =
      { toSlashInvariantForm := toSlashInvariantForm_1, holo' := holo'_1, bdd_at_cusps' := bdd_at_cusps'_1 } →
    toSlashInvariantForm = toSlashInvariantForm_1

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

1 results in Mathlib

Foundations

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