Theorem NumberField.ComplexEmbedding.Extension.not_isReal_of_not_isReal

Modification history

2025-09-19 09:10
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
feat: predicates for extensions of complex embeddings (#27977) …
Added NumberField.ComplexEmbedding.Extension.not_isReal_of_not_isRealView on Github →