Theorems · Theorem · number theory

CuspForm.mk.injEq

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

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

0 results in Mathlib

Foundations

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