Theorem NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramified

Modification history

2026-07-14 17:49
Mathlib/NumberTheory/NumberField/Completion/Ramification.lean
feat(NumberTheory/NumberField/Completion/Ramification): add `InfinitePlace.mult_mul_finrank` (#41600) …
Deleted NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramifiedView on Github →
2026-04-13 19:44
Mathlib/NumberTheory/NumberField/Completion/Ramification.lean
feat: `NumberField.InfinitePlace.sum_inertiaDeg_eq_finrank` (#30551) …
Added NumberField.InfinitePlace.Completion.finrank_eq_one_of_isUnramifiedView on Github →