Inner product space L2([0,1]) with periodic b.c.

Stream: Is there code for X?

[Nicholas Wilson]

I'm trying to figure out how Mathlib does inner product spaces and want to look at an example I understand. Does Mathlib have that as an example somewhere?

[Johan Commelin]

Your title suggest you don't want a random inner product space, but a specific example. Is that right?

[Nicholas Wilson]

I want to use an example as a guide to see how to use it/how it works. I understand the concept on classes/instances but I don't know how to write them.

[Johan Commelin]

Hmm, I'm still confused about what exactly you want. Does docs#InnerProductSpace help? You can click on "Instances" at the bottom of that entry to get a list of instances. Are those useful examples?

[Johan Commelin]

image.png

[Nicholas Wilson]

Oh, I had no idea that the instances thing was there in the docs. I've found the links to the source for those entries.