A ℚ
-vector space has TwoUniqueSums
. #
Any ℚ
-vector space has TwoUniqueSums
, because it is isomorphic to some
(Basis.ofVectorSpaceIndex ℚ G) →₀ ℚ
by choosing a basis, and ℚ
already has
TwoUniqueSums
because it's ordered.