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]( (@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.

Estimated changes