Frobenius inner product

Stream: Is there code for X?

[Daniel Lambert]

Hello, I wonder if there is Frobenius inner product now, like https://en.wikipedia.org/wiki/Frobenius_inner_product. If not, what should I do to define this independently? Which APIs are necessary?

[Jireh Loreaux]

I don't think we have this yet, but it should go in a new file Analysis.InnerProductSpace.Matrix. Note that we already have the norm structure: docs#Matrix.frobeniusNormedAlgebra, so you should hook into that when providing the docs#InnerProductSpace instance. You can create a PR to mathlib, and you can follow the directions at https://leanprover-community.github.io/contribute/index.html

[Daniel Lambert]

Thanks a lot! I'll try it in a few days. Btw, is it necessary to declare as a def instead of an instance? just like those in Mathlib.Analysis.Matrix

[Jireh Loreaux]

Yes, and you'll need to activate the frobenius norm as a local instance.