Extended inner product space doesn't invoke normed group

Stream: new members

[Max Bobbin]

I'm working on defining a structure that extends inner product space and I'm running into a problem where I write the derivative of a function from the field to the vector space and Lean gives an error expecting normed_add_comm_group E but the structure extends inner_product_space which extends normed_add_comm_group. Is there a way to get Lean to recognize is already has normed_add_comm_group E?

MWE:

import analysis.calculus.deriv
import analysis.inner_product_space.basic

noncomputable theory

structure test (𝕜 : Type*) (E : Type*) [is_R_or_C 𝕜]
  extends inner_product_space 𝕜 E :=
(h : 1=1) --just a dummy statement so Lean compiles the structure

example {𝕜 : Type*} {E : Type*} [is_R_or_C 𝕜] [test 𝕜 E] (f : 𝕜 → E) : deriv f = deriv f := --throughs error "failed to synthesize type class instance for normed_add_comm_group E"

[Eric Wieser]

You want class not structure

[Max Bobbin]

Interesting, I wasn't aware there was a difference. I noticed on the front end of the mathlib website it calls it a structure, but all the backend code I looked at will use class, so I assumed they were interchangable. What is the difference between structure and class if you could give a brief explanation?

[Junyan Xu]

I guess class is synonymous to @[class] structure?

[Max Bobbin]

Thank you, found it in the textbook, reading now!