Theorem NumberField.ComplexEmbedding.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) …
Added NumberField.ComplexEmbedding.IsUnmixed.isReal_iff_isRealView on Github →