Theorem Int.absNorm_under_mem

Modification history

2025-06-06 16:43
Mathlib/RingTheory/Ideal/Int.lean
feat(Ideal/Int): some results about ideals of `ℤ` or ideals of extensions of `ℤ` (#25528) …
Added Int.absNorm_under_memView on Github →