Commit 2026-09-23 08:52 7a751b75
View on Github →refactor(RingTheory/RamificationInertia/Ramification): generalize ramificationIdx_pos (#41377)
Positivity of ramification index currently requires Module.Finite, but it is also true for Dedekind domains. This PR extracts a common generalization ramificationIdx_pos_of_mem_minimalPrimes and deduces these two facts as corollaries. This allows for a few more removals of the old ramificationIdx'.