Theorem IsCyclotomicExtension.Rat.inertiaDeg_eq_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) …
Added IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvdView on Github →