Theorem Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn

Modification history

2025-02-13 06:13
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat(NumberTheory/RamificationInertia): `ramificationIdx` and `inertiaDeg` in Galois extensions (#20899) …
Added Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegInView on Github →