Skip to content

Commit

Permalink
chore: remove redundant coercion in SlashInvariantForms (#8376)
Browse files Browse the repository at this point in the history
This coercion is redundant with one already available via a FunLike instance. It's not actually particularly significant by itself, but it is shows up in many typeclass search traces, and because it comes first, obscures more serious problems!



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Nov 13, 2023
1 parent 43e3265 commit b67998a
Showing 1 changed file with 0 additions and 5 deletions.
5 changes: 0 additions & 5 deletions Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean
Expand Up @@ -91,11 +91,6 @@ open SlashInvariantForm

variable {F : Type*} {Γ : outParam <| Subgroup SL(2, ℤ)} {k : outParam ℤ}

instance (priority := 100) SlashInvariantFormClass.coeToFun [SlashInvariantFormClass F Γ k] :
CoeFun F fun _ => ℍ → ℂ :=
FunLike.hasCoeToFun
#align slash_invariant_form.slash_invariant_form_class.coe_to_fun SlashInvariantForm.SlashInvariantFormClass.coeToFun

-- @[simp] -- Porting note: simpNF says LHS simplifies to something more complex
theorem slash_action_eqn [SlashInvariantFormClass F Γ k] (f : F) (γ : Γ) : ↑f ∣[k] γ = ⇑f :=
SlashInvariantFormClass.slash_action_eq f γ
Expand Down

0 comments on commit b67998a

Please sign in to comment.