Commit 2025-10-11 20:00 702b8300

feat: Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing (#29729) We add the special case Ideal.ramificationIdx_mul_inertiaDeg_of_isLocalRing of Ideal.sum_ramification_inertia in the local (DVR) case: the product of the ramification index and the inertia degree equals the degree of the field extension. Also make the argument p implicit in Ideal.sum_ramification_inertia.