Nicolò Cavalleri (Jun 21 2021 at 15:22): Nicolò Cavalleri (Jun 21 2021 at 15:22):If I want to state that two subspaces of two vector spaces are isomorphic there is not an appropriate property in HOL, but I need to state it with linear_on and bij_betw right?
Nicolò Cavalleri (Jun 22 2021 at 20:14):And similarly there is no isomorphism of vector spaces, is there?
Last updated: Dec 08 2025 at 08:34 UTC