Commit 2024-10-26 11:58 83461cc0

View on Github →

feat: miscellaneous results about inertia degree (#18111) From flt-regular.

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia.lean

added theorem Ideal.inertiaDeg_comap_eq

added theorem Ideal.ramificationIdx_comap_eq

Modified Mathlib/RingTheory/Ideal/Maps.lean

added theorem Ideal.comap_coe