Theorem Algebra.IsUnramifiedIn.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.ramificationIdx_eq_one View on Github →

2026-06-22 15:26

Mathlib/NumberTheory/RamificationInertia/Unramified.lean

feat: add Algebra.IsUnramifiedIn (#40886)

Added Algebra.IsUnramifiedIn.ramificationIdx_eq_one View on Github →