Def Ideal.Quotient.algEquivOfEqMap

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.Quotient.algEquivOfEqMap View on Github →