Theorem Algebra.IsUnramifiedIn.ramificationIdx_eq_one

Modification history

2026-10-08 13:29
Mathlib/NumberTheory/RamificationInertia/Unramified.lean
chore: weaken hypotheses of Algebra.IsUnramifiedIn.ramificationIdx_eq_one (#41578) …
Modified Algebra.IsUnramifiedIn.ramificationIdx_eq_oneView on Github →
2026-06-30 12:19
Mathlib/NumberTheory/RamificationInertia/Unramified.lean
refactor(NumberTheory/RamificationInertia/Unramified): switch to new definition of ramification index (#41191) …
Modified Algebra.IsUnramifiedIn.ramificationIdx_eq_oneView on Github →
2026-06-22 15:26
Mathlib/NumberTheory/RamificationInertia/Unramified.lean
feat: add Algebra.IsUnramifiedIn (#40886)
Added Algebra.IsUnramifiedIn.ramificationIdx_eq_oneView on Github →