Stream: math-comp analysis

Topic: `vectType R` and `normedModType R`

view this post on Zulip abab9579 (Sep 11 2022 at 23:12):

Does vectType R not have normedModType structure? I want to work on finite-dimensional vectorspace structure instead of direct R^n.+1. Is this because trivial vectorspace does not have normedModType structure?

Last updated: Feb 05 2023 at 13:02 UTC