Theorem NumberField.InfinitePlace.comp_of_comap_eq

Modification history

2025-05-14 09:01
Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean
feat: basic `InfinitePlace.comap` lemmas (#24879)
Added NumberField.InfinitePlace.comp_of_comap_eqView on Github →