Theorem Ideal.coe_smul_primesOver_eq_map_galRestrict

Modification history

2025-07-04 10:05

Mathlib/NumberTheory/RamificationInertia/Galois.lean

chore: whitespace before `:` (#26727) …

Modified Ideal.coe_smul_primesOver_eq_map_galRestrict 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.coe_smul_primesOver_eq_map_galRestrict View on Github →