Commit 2024-12-10 15:20 14375b94

View on Github →

refactor/fix: don't use RingHom.toAlgebra in Ideal.quotientAlgebra (#19847)

Estimated changes

Modified Mathlib/NumberTheory/RamificationInertia/Basic.lean

modified def Ideal.Quotient.algebraQuotientOfRamificationIdxNeZero

modified theorem Ideal.inertiaDeg_algebraMap

modified theorem Ideal.inertiaDeg_comap_eq

modified theorem Ideal.inertiaDeg_map_eq

modified theorem Ideal.inertiaDeg_pos

deleted theorem Ideal.inertiaDeg_tower

Modified Mathlib/RingTheory/Ideal/Over.lean

deleted def Ideal.Quotient.algebraQuotientOfLEComap

Modified Mathlib/RingTheory/Ideal/Quotient/Operations.lean