Theorem Algebra.isUnramifiedIn_iff_forall_ramificationIdx_eq_one

Modification history

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_iff_forall_ramificationIdx_eq_oneView on Github →
2026-06-22 15:26
Mathlib/NumberTheory/RamificationInertia/Unramified.lean
feat: add Algebra.IsUnramifiedIn (#40886)
Added Algebra.isUnramifiedIn_iff_forall_ramificationIdx_eq_oneView on Github →