mathlib

7265a4ee - feat(linear_algebra/dimension): generalize inequalities and invariance of dimension to arbitrary rings (#8343)

feat(linear_algebra/dimension): generalize inequalities and invariance of dimension to arbitrary rings (#8343) We implement some of the results of [_Les familles libres maximales d'un module ont-elles le meme cardinal?_](http://www.numdam.org/article/PSMIR_1973___4_A4_0.pdf). We also generalize many theorems which were previously proved only for vector spaces, but are true for modules over arbitrary rings or rings satisfying the (strong) rank condition or have invariant basis number. (These typically need entire new proofs, as the original proofs e.g. used rank-nullity.) The main new results are: * `basis_fintype_of_finite_spans`: Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite. * `union_support_maximal_linear_independent_eq_range_basis`: Over any ring `R`, if `b` is a basis for a module `M`, and `s` is a maximal linearly independent set, then the union of the supports of `x ∈ s` (when written out in the basis `b`) is all of `b`. * `infinite_basis_le_maximal_linear_independent`: Over any ring `R`, if `b` is an infinite basis for a module `M`, and `s` is a maximal linearly independent set, then the cardinality of `b` is bounded by the cardinality of `s`. * `mk_eq_mk_of_basis`: We generalize the invariance of dimension theorem to any ring with the invariant basis number property. * `basis.le_span`: We generalize this statement (the size of a basis is bounded by the size of any spanning set) to any ring satisfying the rank condition. * `linear_independent_le_span`: If `R` satisfies the strong rank condition, then for any linearly independent family `v : ι → M` and any finite spanning set `w : set M`, the cardinality of `ι` is bounded by the cardinality of `w`. * `linear_independent_le_basis`: Over any ring `R` satisfying the strong rank condition, if `b` is a basis for a module `M`, and `s` is a linearly independent set, then the cardinality of `s` is bounded by the cardinality of `b`. There is a naming discrepancy: most of the theorem names refer to `dim`, even though the definition is of `module.rank`. This reflects that `module.rank` was originally called `dim`, and only defined for vector spaces. I would prefer to address this in a separate PR (note this discrepancy wasn't introduced in this PR). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>