Theorem IntermediateField.isSimpleOrder_of_finrank_prime

Modification history

2025-07-06 09:09
Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
feat(NumberField/CMField): All CM-extensions come from the real maximal subfield (#25818) …
Added IntermediateField.isSimpleOrder_of_finrank_primeView on Github →