Mathlib Changelog
v4
Changelog
About
Github
Theorem
Ideal.isPretransitive_of_isGalois
Modification history
2025-02-13 06:13
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions (#20899) …
Added
Ideal.isPretransitive_of_isGalois
View on Github →