feat(linear_algebra/dual): add dual vector spaces (#881)
* feat(linear_algebra/dual): add dual vector spaces
Define dual modules and vector spaces and prove the basic theorems: the dual basis isomorphism and
evaluation isomorphism in the finite dimensional case, and the corresponding (injectivity)
statements in the general case. A variant of `linear_map.ker_eq_bot` and the "inverse" of
`is_basis.repr_total` are included.
Universe issues make an adaptation of `linear_equiv.dim_eq` necessary.
* style(linear_algebra/dual): adapt to remarks from PR dsicussion
* style(linear_algebra/dual): reformat proof of `ker_eq_bot'`
