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)
@[deprecated Subalgebra.isSimpleOrder_of_finrank_prime (since := "2024-08-11")]
theorem
FiniteDimensional.Subalgebra.is_simple_order_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)