Theorems · Definition · number theory

CuspForm.mk.noConfusion

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

Defined in

Mathlib.NumberTheory.ModularForms.Basic

Cited by

1 results in Mathlib

Foundations

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