refactor(linear_algebra/*): more generalisations (#13668)
Many further generalisations from `field` to `division_ring` in the linear algebra library.
This PR changes some proofs; it's not just relaxing hypotheses.
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
