mathlib

c4658a64 - feat(linear_algebra/finite_dimensional): generalize from field to division_ring and more (#17401)

feat(linear_algebra/finite_dimensional): generalize from field to division_ring and more (#17401) + Replace K by ℕ in two proofs in *linear_algebra/basis*, which immediately allows generalization from `division_ring` to `field` in *submodule/basic*, *field_theory/tower*, *linear_algebra/dimension*, *projective_space/basic*, *linear_algebra/finite_dimensional*, and *affine_space/finite_dimensional*. (~~@riccardobrasca authored many of these;~~ @semorrison made some `division_ring` generalizations a while ago; @adamtopaz's TODO in *projective_space/basic* is now resolved. Let me know if you can think of more stuff to generalize.) + Add `subalgebra.is_simple_order_of_finrank_prime` in *field_theory/tower*. Inspired by [#17237](https://github.com/leanprover-community/mathlib/pull/17237#discussion_r1009097091) (@xroblot). + Make `subalgebra.to_submodule` an `order_embedding` in *subalgebra/basic*, remove lemmas rendered redundant, and fix things in *intermediate_field*, *field_theory/normal*, and *adjoin/fg*. + Changes in *linear_algebra/finite_dimensional* and *linear_algebra/finrank*: + Add `finite_dimensional_of_dim_eq_nat`: used to golf `finite_dimensional_of_dim_eq_zero/one`. + Add `submodule.finrank_le_finrank_of_le` and `finrank_lt_finrank_of_lt` which only assumes the larger submodule is finite rather than the whole module. Rename the original `finrank_lt_finrank_of_lt` to `finrank_strict_mono`, matching the existing `finrank_mono`. + Remove `subalgebra.dim/finrank_eq_one_of_eq_bot` which has a substitutable equality among its assumptions (use `dim/finrank_bot` instead). + Add `subalgebra.dim/finrank/finite_dimensional_to_submodule` and an instance `finite_dimensional_subalgebra` similar to [finite_dimensional_submodule](https://leanprover-community.github.io/mathlib_docs/linear_algebra/finite_dimensional.html#finite_dimensional.finite_dimensional_submodule). + Generalize `section subalgebra_dim` from `[field E]` to `[ring E]`, adding `[nontrivial E]` hypothesis whenever necessary. + Generalize `subalgebra.eq_bot_of_dim_one` to `of_dim_le_one` and golf the proof (together with `eq_bot_of_finrank_one`). + Move `finite_dimensional.of_subalgebra_to_submodule` from *splitting_field* to *finite_dimensional*. + Add `exists_nat_eq_of_le_nat` in *cardinal/basic*. + Fix a slow proof in *polynomial/bernstein*. Co-authored-by: Xavier-François Roblot <46200072+xroblot@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>