Real vector space (source code)

= Real vector space

A real vector space is a <vector space> over the <field> $\mathbb R$ of <real numbers>.