Commit 2022-11-19 17:26 c4658a64

View on Github →

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