Commit 2026-06-04 10:17 5135da2b

View on Github →

feat(RingTheory/RamificationInertia/Ramification): positivity of ramification index (#39977) This PR proves positivity of the new definition of ramification index.

Estimated changes

Modified Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean

added theorem PrimeSpectrum.coe_primesOverOrderIsoFiber_symm_apply

Modified Mathlib/RingTheory/RamificationInertia/Ramification.lean

added theorem Ideal.ramificationIdx'_pos