Theorem NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one

Modification history

2025-07-11 22:12
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
feat(NumberField/CMField): A totally complex abelian extension of ℚ is CM (#26073) …
Added NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_oneView on Github →