-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(finite_dimensional/subalgebra) : add subalgebra.is_simple_order_of_finrank #17237
Conversation
0ae90f4
to
759a84e
Compare
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
maintainer merge |
🚀 Pull request has been placed on the maintainer queue by alreadydone. |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Comments are not loading on my phone so maybe you already addressed this: is there no |
Comments are not loading on my phone so maybe you already addressed this: is there no LGTM otherwise! bors d+ |
✌️ xroblot can now approve this pull request. To approve and merge a pull request, simply reply with |
I found versions of Well, I just did that :) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
That generality is much better, thanks! Once the build passes, please reply with bors merge
to merge this pull request.
bors merge |
…of_finrank (#17237) This PR adds some lemma that will be used in the proof (#17285) that two complex embeddings of a field define the same place iff they are equal or complex conjugate, mainly: - `subalgebra.is_simple_order_of_finrank` shows that the only two subalgebras in an algebra of dimension 2 are exactly `⊥` and `⊤`
Pull request successfully merged into master. Build succeeded: |
…ision_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](#17237 (comment)) (@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>
This PR adds some lemma that will be used in the proof (#17285) that two complex embeddings of a field define the same place iff they are equal or complex conjugate, mainly:
subalgebra.is_simple_order_of_finrank
shows that the only two subalgebras in an algebra of dimension 2 are exactly⊥
and⊤