Metamath Proof Explorer

Table of Contents - 21.20.8.1. Real vector spaces

In this section, we introduce real vector spaces.

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