Theorem Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn

Modification history

2025-11-09 18:05

Mathlib/NumberTheory/RamificationInertia/Galois.lean

refactor(NumberTheory/RamificationInertia/Galois): switch to `IsGaloisGroup G A B` (#30934) …

Modified Ideal.ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn View on Github →

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