Theorem NumberField.InfinitePlace.IsUnramified.finrank_eq_one

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.IsUnramified.finrank_eq_oneView on Github →
2026-07-14 17:49
Mathlib/NumberTheory/NumberField/Completion/Ramification.lean
feat(NumberTheory/NumberField/Completion/Ramification): add `InfinitePlace.mult_mul_finrank` (#41600) …
Added NumberField.InfinitePlace.IsUnramified.finrank_eq_oneView on Github →