Theorem NumberField.ComplexEmbedding.Extension.conjugate_comp_ne

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.conjugate_comp_neView on Github →