Commit 2021-09-07 16:31 463e7534

View on Github →

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).

Estimated changes

Modified src/analysis/normed_space/finite_dimension.lean

Modified src/field_theory/finite/polynomial.lean

Modified src/linear_algebra/dimension.lean

added theorem dim_eq_card_basis

deleted theorem dim_of_ring

modified theorem dim_quotient_le

added theorem dim_self

Modified src/linear_algebra/finite_dimensional.lean

deleted theorem finite_dimensional.dim_eq_card_basis

modified theorem finite_dimensional.finite_dimensional_of_finrank

modified theorem finite_dimensional.finrank_eq_dim

deleted theorem finite_dimensional.finrank_of_field

modified theorem finite_dimensional.finrank_of_infinite_dimensional

added theorem finite_dimensional.finrank_self

modified theorem finite_dimensional.of_finset_basis

modified def finite_dimensional

Modified src/measure_theory/measure/hausdorff.lean