Commit 2026-07-15 01:20 11d11a11

View on Github →

chore(NumberTheory/NumberField/InfinitePlace/Basic): add abbrev of LiesOver for InfinitePlace (#41747) This PR adds an abbrev of LiesOver for InfinitePlace.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/Completion/InfinitePlace.lean

Modified Mathlib/NumberTheory/NumberField/Completion/LiesOverInstances.lean

Modified Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

modified theorem NumberField.InfinitePlace.IsRamified.finrank_eq_two

modified theorem NumberField.InfinitePlace.IsUnramified.finrank_eq_one

modified theorem NumberField.InfinitePlace.inertiaDeg_eq_finrank

modified theorem NumberField.InfinitePlace.inertiaDeg_of_liesOver

modified theorem NumberField.InfinitePlace.mult_mul_finrank

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Ramification.lean

modified def NumberField.InfinitePlace.placesOver

modified def NumberField.InfinitePlace.ramifiedPlacesOver

modified def NumberField.InfinitePlace.unramifiedPlacesOver