Commit 2026-02-18 13:41 6c31aede

View on Github →

chore(RamificationInertia): remove an unnecessary hypothesis in inertiaDeg_algebraMap (#35483)

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

modified theorem Ideal.inertiaDeg_algebraMap

modified theorem Ideal.inertiaDeg_comap_eq

modified theorem Ideal.inertiaDeg_map_eq

Modified Mathlib/NumberTheory/RamificationInertia/Galois.lean

modified theorem Ideal.inertiaDegIn_eq_inertiaDeg

modified theorem Ideal.inertiaDeg_eq_of_isGaloisGroup