mathlib3

463e7534 - feat(linear_algebra/finite_dimensional): generalisations to division_ring (#8822)

feat(linear_algebra/finite_dimensional): generalisations to division_ring (#8822) I generalise a few results about finite dimensional modules from fields to division rings. Mostly this is me trying out @alexjbest's `generalisation_linter`. (review: it works really well, and is very helpful for finding the right home for lemmas, but it is slow). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>