Zulip Chat Archive

Stream: new members

Topic: Extended inner product space doesn't invoke normed group

Max Bobbin (Jul 29 2022 at 17:55):

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?


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 (Jul 29 2022 at 18:00):

You want class not structure

Max Bobbin (Jul 29 2022 at 18:02):

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 (Jul 29 2022 at 18:16):

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

Max Bobbin (Jul 29 2022 at 19:00):

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

Last updated: Dec 20 2023 at 11:08 UTC