Theorem Ideal.card_inertia_eq_ramificationIdxIn

Modification history

2026-06-18 11:44

Mathlib/NumberTheory/RamificationInertia/Galois.lean

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

Modified Ideal.card_inertia_eq_ramificationIdxIn View on Github →

2025-10-26 15:49

Mathlib/NumberTheory/RamificationInertia/Galois.lean

feat(NumberTheory): order of inertia group = ramification index (#30675)

Added Ideal.card_inertia_eq_ramificationIdxIn View on Github →