If A is a domain, and a finite-dimensional algebra over a field F, with prime dimension, then there are no non-trivial F-subalgebras.

theorem Subalgebra.isSimpleOrder_of_finrank_prime (F : Type u_1) (A : Type u_2) [Field F] [Ring A] [IsDomain A] [Algebra F A] (hp : Nat.Prime (Module.finrank F A)) : IsSimpleOrder (Subalgebra F A)