Theorem Ideal.ncard_primesOver_mul_ncard_primesOver

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_ncard_primesOverView on Github →
2025-12-03 12:39
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(RamificationInertia): multiplicativity of indices in a tower of Galois extensions (#32309) …
Added Ideal.ncard_primesOver_mul_ncard_primesOverView on Github →