Theorem IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'

Modification history

2026-07-04 11:51

Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

refactor(RingTheory/RamificationInertia/Inertia): swap `inertiaDeg` and `inertiaDeg'` (#41325) …

Modified IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'View on Github →

2026-06-18 11:44

Mathlib/NumberTheory/NumberField/Cyclotomic/Ideal.lean

feat(NumberTheory/RamificationInertia/Galois): ramification inertia refactor (#40126) …

Modified IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'View on Github →

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_span_zeta_sub_one'View on Github →