A ℚ-vector space has TwoUniqueSums.

instance instTwoUniqueSumsOfModuleRat {G : Type u_1} [AddCommGroup G] [Module ℚ G] : TwoUniqueSums G

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.

Equations

• ⋯ = ⋯