Theorem Ideal.spanNorm_le_comap

Modification history

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 →