Theorem Ideal.relNorm_le_comap

Modification history

2025-10-09 08:14
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat: remove separability assumption from Algebra.isIntegral_norm (#30323) …
Modified Ideal.relNorm_le_comapView on Github →
2025-08-22 16:49
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat(RingTheory/Ideal): prove transitivity for the relative norm (#27152) …
Added Ideal.relNorm_le_comapView on Github →