Commit 2026-03-11 20:49 b495b14b

feat(RamificationInertia): add ramificationIdx_algebra_tower' (#35493) The result Ideal.ramificationIdx_algebra_tower is stated in a very general situation whereas most of its applications should be when there is a tower of prime ideals like in Ideal.inertiaDeg_algebra_tower. This PR adds a version of Ideal.ramificationIdx_algebra_tower specialized to this case. The instances needed are stronger but there is no side condition. I believe that this corresponds to the more useful situation and thus I replaced all the use of Ideal.ramificationIdx_algebra_tower by the new version even if that means having to adjust the hypotheses.