Theorem NumberField.IsCMField.ofCMExtension

Modification history

2025-12-05 13:19
Mathlib/NumberTheory/NumberField/CMField.lean
feat(CMField): add `IsCyclotomicExtension.Rat.isCMField` (#31812) …
Modified NumberField.IsCMField.ofCMExtensionView on Github →
2025-09-18 14:30
Mathlib/NumberTheory/NumberField/CMField.lean
chore(NumberField/CMField): refactor (#29746) …
Modified NumberField.IsCMField.ofCMExtensionView on Github →
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.IsCMField.ofCMExtensionView on Github →