Theorem Ideal.spanNorm_le_comap

Modification history

2025-10-27 15:31
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat: remove separability assumption from Algebra.dvd_algebraMap_intNorm_self (#30478) …
Modified Ideal.spanNorm_le_comapView on Github →
2025-10-09 08:14
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat: remove separability assumption from Algebra.isIntegral_norm (#30323) …
Modified Ideal.spanNorm_le_comapView on Github →
2025-08-16 16:09
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat(Algebra/intNorm): `x` divides `intNorm x` (#28021) …
Added Ideal.spanNorm_le_comapView on Github →