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.