Theorem Ideal.LiesOver.of_eq_comap

Modification history

2024-11-04 21:50

Mathlib/RingTheory/Ideal/Over.lean

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

Added Ideal.LiesOver.of_eq_comap View on Github →