A vector space over a field \( F \) is a non-empty set \( V \) with a binary operation \( \oplus \) on \( V \) and a binary function \( \otimes : F \times V \to V \) such that the following hold for any \( a, b \in F \) and \( u , v \in V \)

• \( \oplus \) is associative and commutative
• There is a identity element \( 0 _ V \) with respect to \( \oplus \)
• \( 1 _ F \) is an identity element for \( \otimes \)
• \( \oplus \) has inverses for \( 0 _ V \)
• \( \otimes \) distributes into \( \oplus \)
• \( \left( a + _ F b \right) \otimes v = \left( a \otimes v \right) \oplus \left( b \otimes v \right) \)
• \( a \otimes \left( b \otimes v \right) = \left( a \cdot _ F b \right) \otimes v \)