Theorem NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eq
Modification history
2025-10-29 12:03
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean
feat(InfinitePlace/Ramification): `LiesOver` class for absolute values and derived results on infinite places (#27978) …
Added NumberField.InfinitePlace.LiesOver.embedding_comp_eq_or_conjugate_embedding_comp_eqView on Github →