Theorem Ideal.ramificationIdx_map_eq

Modification history

2026-03-25 22:20

Mathlib/NumberTheory/RamificationInertia/Basic.lean

chore(NumberTheory/RamificationInerta/Basic): split file (#37173) …

Modified Ideal.ramificationIdx_map_eq View on Github →

2026-03-25 11:32

Mathlib/NumberTheory/RamificationInertia/Basic.lean

refactor(NumberTheory/RamificationInertia/Basic): remove the ring homomorphism from `Ideal.ramificationIdx` (#37156) …

Modified Ideal.ramificationIdx_map_eq View on Github →

2024-11-04 21:50

Mathlib/NumberTheory/RamificationInertia.lean

refactor(NumberTheory/RamificationInertia): use `Ideal.LiesOver` in some results about `inertiaDeg` (#18270) …

Added Ideal.ramificationIdx_map_eq View on Github →