Theorem NumberField.IsCMField.IsCyclotomicExtension.Rat.isCMField

Modification history

2025-12-05 13:19
Mathlib/NumberTheory/NumberField/CMField.lean
feat(CMField): add `IsCyclotomicExtension.Rat.isCMField` (#31812) …
Added NumberField.IsCMField.IsCyclotomicExtension.Rat.isCMFieldView on Github →