Theorem Int.absNorm_under_dvd_absNorm

Modification history

2026-10-23 16:22
Mathlib/RingTheory/Ideal/Int.lean
chore(RingTheory/Ideal): drop the infiniteness assumption from the results using `Ideal.absNorm` (#44646) …
Modified Int.absNorm_under_dvd_absNormView on Github →
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 →