Theorem NumberField.ComplexEmbedding.Extension.comp_eq

Modification history

2026-03-04 10:41
Mathlib/NumberTheory/NumberField/InfinitePlace/Embeddings.lean
feat(InfinitePlace/Completion): embeddings of `w.Completion` factor through embeddings of `v.Completion` when `w` lies over `v` (#29942) …
Modified NumberField.ComplexEmbedding.Extension.comp_eqView 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.comp_eqView on Github →