Commit 2026-01-11 14:20 8ea945b3

feat(RingTheory/Localization/AtPrime): inertia degree and ramification index are preserved by localization (#27706) Let R ⊆ S be an extension of rings and p be a prime ideal of R. Denote by Rₚ the localization of R at the complement of p and by Sₚ the localization of S at the (image) of the complement of p. In this PR, we prove that the bijection between the (nonzero) prime ideals of Sₚ and the prime ideals of S above p preserves the residual degree and the ramification index.