Theorem NumberField.CMExtension.eq_maximalRealSubfield

Modification history

2025-07-06 09:09
Mathlib/NumberTheory/NumberField/CMField.lean
feat(NumberField/CMField): All CM-extensions come from the real maximal subfield (#25818) …
Added NumberField.CMExtension.eq_maximalRealSubfieldView on Github →