We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent be88371 commit 9a5f3d4Copy full SHA for 9a5f3d4
1 file changed
Mathlib/NumberTheory/NumberField/CMField.lean
@@ -41,7 +41,7 @@ subfield `F` is (isomorphic to) the maximal real subfield `K⁺` of `K`.
41
42
* `NumberField.IsCMField.of_isMulCommutative`: A totally complex abelian extension of `ℚ` is CM.
43
44
-* `IsCyclotomicExtension.Rat.isCMField`: A nontrivial abelian extension of `ℚ` is CM.
+* `IsCyclotomicExtension.Rat.isCMField`: A nontrivial cyclotomic extension of `ℚ` is CM.
45
46
## Implementation note
47
@@ -561,7 +561,7 @@ variable (K : Type*) [Field K] [CharZero K]
561
562
open IntermediateField in
563
/--
564
-A nontrivial abelian extension of `ℚ` is CM.
+A nontrivial cyclotomic extension of `ℚ` is CM.
565
-/
566
theorem isCMField {S : Set ℕ} (hS : ∃ n ∈ S, 2 < n) [IsCyclotomicExtension S ℚ K] :
567
IsCMField K := by
0 commit comments