Commit 2026-05-04 20:38 98ac701b
View on Github →feat(RingTheory/RamificationInertia): alternate definitions of ramification index and inertia degree (#38062) This PR adds alternate definitions of ramification index and inertia degree, following the discussion here: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Improving.20the.20definition.20of.20ramification.20index.3F