Theorem Ideal.map_spanIntNorm

Modification history

2025-03-17 19:45
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat: generalize CommRing to Ring/Semiring (#22566) …
Modified Ideal.map_spanIntNormView on Github →
2025-02-03 10:21
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat: generalize `Ideal.spanNorm` to allow non free extensions (#19244) …
Added Ideal.map_spanIntNormView on Github →