Commit 2025-10-27 15:31 529ccf07

View on Github →

feat: remove separability assumption from Algebra.dvd_algebraMap_intNorm_self (#30478) Continuing the work of #30323 and #30448 we remove the separability assumption from Algebra.dvd_algebraMap_intNorm_self.

Estimated changes

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

modified theorem Ideal.relNorm_le_comap

modified theorem Ideal.spanNorm_le_comap

Modified Mathlib/RingTheory/IntegralClosure/IntegralRestrict.lean

modified theorem Algebra.dvd_algebraMap_intNorm_self