Theorem Ideal.coe_smul_primesOver_eq_map_galRestrict

Modification history

2025-10-16 07:33
Mathlib/NumberTheory/RamificationInertia/Galois.lean
feat: notation for galois group (#30266) …
Modified Ideal.coe_smul_primesOver_eq_map_galRestrictView on Github →
2025-07-04 10:05
Mathlib/NumberTheory/RamificationInertia/Galois.lean
chore: whitespace before `:` (#26727) …
Modified Ideal.coe_smul_primesOver_eq_map_galRestrictView 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_galRestrictView on Github →