Theorem NumberField.ComplexEmbedding.Extension.IsUnmixed.isReal_iff_isReal

Modification history

2025-09-28 12:07
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
feat(InfinitePlace/Embeddings): remove dependency of `IsMixed`/`IsUnmixed` on `Extension`. (#29945) …
Deleted NumberField.ComplexEmbedding.Extension.IsUnmixed.isReal_iff_isRealView on Github →
2025-09-19 09:10
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
feat: predicates for extensions of complex embeddings (#27977) …
Added NumberField.ComplexEmbedding.Extension.IsUnmixed.isReal_iff_isRealView on Github →