mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore(analysis/normed_space/inner_product): euclidean space is a real inner product space

Open urkud opened this issue 4 years ago • 2 comments

Open in Gitpod

urkud avatar Mar 21 '21 05:03 urkud

Oh, I guess [Π i, inner_product_space ℝ (f i)] [Π i, inner_product_space 𝕜 (f i)] is illegal because it puts two different additive group structures on f i...

eric-wieser avatar Mar 14 '23 10:03 eric-wieser

I don't remember why I wanted this. I remember that I didn't use these instances in the final version, then abandoned this pr. We can close it if it leads to diamonds.

urkud avatar Mar 15 '23 20:03 urkud