Theorem IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow

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.inertiaDegIn_eq_of_prime_powView on Github →