Def NumberField.InfinitePlace.ramifiedPlacesOver

Modification history

2026-03-21 05:43

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

feat(NumberField/InfinitePlace/Ramification): add cardinality results for (un)ramified places over (#36353) …

Modified NumberField.InfinitePlace.ramifiedPlacesOver View on Github →

2026-03-05 14:29

Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

feat(NumberField/InfinitePlace/Ramification): add `placesOver` (#36132) …

Added NumberField.InfinitePlace.ramifiedPlacesOver View on Github →