Theorem Ideal.ncard_primesOver_mul_card_inertia_mul_finrank

Modification history

2026-06-18 11:44

Mathlib/NumberTheory/RamificationInertia/Galois.lean

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

Modified Ideal.ncard_primesOver_mul_card_inertia_mul_finrank View on Github →

2025-10-26 15:49

Mathlib/NumberTheory/RamificationInertia/Galois.lean

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

Added Ideal.ncard_primesOver_mul_card_inertia_mul_finrank View on Github →