Theorem NumberField.InfinitePlace.comap_apply

Modification history

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