Theorem Ideal.coe_smul_primesOver_mk

Modification history

2025-06-17 04:38

Mathlib/NumberTheory/RamificationInertia/Galois.lean

refactor(NumberTheory/RamificationInertia/Galois): Generalize action on `primesOver` to arbitrary group (#25995) …

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