Commit 2026-07-04 11:51 faaff5e5

View on Github →

refactor(RingTheory/RamificationInertia/Inertia): swap inertiaDeg and inertiaDeg' (#41325) This PR swaps inertiaDeg and inertiaDeg'.

Estimated changes

added theorem Ideal.inertiaDeg'_bot
added theorem Ideal.inertiaDeg'_pos'
added theorem Ideal.inertiaDeg'_pos
deleted theorem Ideal.inertiaDeg_bot
deleted theorem Ideal.inertiaDeg_comap_eq
deleted theorem Ideal.inertiaDeg_map_eq
deleted theorem Ideal.inertiaDeg_ne_zero
deleted theorem Ideal.inertiaDeg_pos'
deleted theorem Ideal.inertiaDeg_pos
deleted theorem Ideal.inertiaDeg'_def
deleted theorem Ideal.inertiaDeg'_eq
deleted theorem Ideal.inertiaDeg'_pos
deleted theorem Ideal.inertiaDeg'_smul
deleted theorem Ideal.inertiaDeg'_tower
added theorem Ideal.inertiaDeg_def
added theorem Ideal.inertiaDeg_eq
added theorem Ideal.inertiaDeg_pos
added theorem Ideal.inertiaDeg_smul
added theorem Ideal.inertiaDeg_tower
deleted theorem Ideal.pow_inertiaDeg'
added theorem Ideal.pow_inertiaDeg