Theorem IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime

Modification history

2025-10-29 08:27
Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean
chore(NumberField/Cyclotomic): add statements for the case of power one (#30996)
Added IsCyclotomicExtension.Rat.inertiaDeg_eq_of_primeView on Github →