Theorem Ideal.Quotient.algebraMap_mk_of_liesOver

Modification history

2025-06-19 11:54
Mathlib/RingTheory/Ideal/Over.lean
feat(RingTheory/DedekindDomain): a prime divides the different ideal iff it is ramified (#25936)
Added Ideal.Quotient.algebraMap_mk_of_liesOverView on Github →