extending an instance

Stream: general

[Chris Birkbeck]

This is probably a very basic question, but I'm wondering about the best way to extend instances. I have a slash_invariant_form structure and a modular_form which extends it. I now want to prove an instance of has_add for each. Is there a way to make use of the extends? Specifically, I have:

variables (F : Type*) (Γ : subgroup SL(2, ℤ)) (k : ℤ)

structure slash_invariant_form :=
(to_fun : ℍ → ℂ)
(slash_action_eq' : ∀ γ : Γ, to_fun ∣[k, γ] = to_fun)

instance has_add : has_add (slash_invariant_form Γ k) := sorry --Say I have this

--Can I use this to make the following easier (i.e. only prove that `mdifferentible` and `bdd_` behaves well?

structure modular_form extends slash_invariant_form Γ k :=
(hol' : mdifferentiable 𝓘(ℂ) 𝓘(ℂ) (to_fun : ℍ → ℂ))
(bdd_at_infty' : ∀ (A : SL(2, ℤ)), is_bounded_at_im_infty (to_fun ∣[k, A]))

instance modular_form.has_add : has_add (modular_form Γ k) := sorry

It feels that I should be able to use the fact that modular_form extends slash_invariant_form to make it so that, if I define the add the same way, then I only need to check that hol' and bdd_at_infty' are additive, but I'm not sure how to do this.

[Eric Wieser]

Have a look at how docs#continuous_linear_map.has_add is defined

[Eric Wieser]

In general, you define the addition as λ x y, { new_field := _, .. x.to_foo + y.to_foo } for old-style structures, or λ x y, { new_field := _, to_foo := x.to_foo + y.to_foo } for new-style structures.

[Chris Birkbeck]

perfect thats what I was looking for!

[Eric Wieser]

Note that for things with to_fun we tend to prefer "old" style (set_option old_structure_cmd true)