Theorem Ideal.intNorm_mem_spanNorm

Modification history

2025-02-03 10:21
Mathlib/RingTheory/Ideal/Norm/RelNorm.lean
feat: generalize `Ideal.spanNorm` to allow non free extensions (#19244) …
Added Ideal.intNorm_mem_spanNormView on Github →