mathlib

6d8e6ead - feat(finite_dimensional/subalgebra) : add subalgebra.is_simple_order_of_finrank (#17237)

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 `⊤`