Commit 2022-11-02 17:10 6d8e6ead

feat(finite_dimensional/subalgebra) : add subalgebra.is_simple_order_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 ⊤