Documentation

Mathlib.Algebra.Group.UniqueProds.VectorSpace

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.