Theorem NumberField.InfinitePlace.inertiaDeg_of_liesOver

Modification history

2026-07-15 01:20

Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

chore(NumberTheory/NumberField/InfinitePlace/Basic): add abbrev of `LiesOver` for `InfinitePlace` (#41747) …

Modified NumberField.InfinitePlace.inertiaDeg_of_liesOver View on Github →

2026-04-13 19:44

Mathlib/NumberTheory/NumberField/Completion/Ramification.lean

feat: `NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank` (#30551) …

Added NumberField.InfinitePlace.inertiaDeg_of_liesOver View on Github →