Metamath Proof Explorer


Table of Contents - 20.16.8.1. Real vector spaces

In this section, we introduce real vector spaces.

  1. bj-fvimacnv0
  2. bj-isvec
  3. bj-flddrng
  4. bj-rrdrg
  5. bj-isclm
  6. crrvec
  7. df-bj-rvec
  8. bj-isrvec
  9. bj-rvecmod
  10. bj-rvecssmod
  11. bj-rvecrr
  12. bj-isrvecd
  13. bj-rvecvec
  14. bj-isrvec2
  15. bj-rvecssvec
  16. bj-rveccmod
  17. bj-rvecsscmod
  18. bj-rvecsscvec
  19. bj-rveccvec
  20. bj-rvecssabl
  21. bj-rvecabl