Theorem NumberField.IsCMField.of_forall_isConj

Modification history

2025-10-16 07:33
Mathlib/NumberTheory/NumberField/CMField.lean
feat: notation for galois group (#30266) …
Modified NumberField.IsCMField.of_forall_isConjView on Github →
2025-09-18 14:30
Mathlib/NumberTheory/NumberField/CMField.lean
chore(NumberField/CMField): refactor (#29746) …
Modified NumberField.IsCMField.of_forall_isConjView on Github →
2025-07-11 22:12
Mathlib/NumberTheory/NumberField/CMField.lean
feat(NumberField/CMField): A totally complex abelian extension of ℚ is CM (#26073) …
Added NumberField.IsCMField.of_forall_isConjView on Github →