Commit 2026-05-11 16:38 686c76b3
View on Github →feat(RingTheory/RamificationInertia/Inertia): add inertiaDeg'_pos (#39073)
This PR adds a positivity lemma for the new inertiaDeg' (which will eventually replace inertiaDeg).
An extra import is needed to synthesize finiteness on the residue fields.