Theorem Int.absNorm_under_dvd_absNorm

Modification history

2026-08-31 14:42
Mathlib/RingTheory/Ideal/Int.lean
chore(RingTheory/Ideal/Norm): weaken `Ideal.absNorm` to infinite Dedekind domains (#42787) …
Modified Int.absNorm_under_dvd_absNormView on Github →
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_dvd_absNormView on Github →