Theorem IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd

Modification history

2025-12-03 17:53
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
feat(CyclotomicField): splitting of the prime `p` in a cyclotomic field `ℚ(ζₙ)` (#32217) …
Deleted IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvdView on Github →
2025-11-27 13:47
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
feat(CyclotomicField): splitting of the prime `p` in `ℚ⟮ζₘ⟯` when `p` does not divide `m` (#31946) …
Added IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvdView on Github →