Theorem Ideal.finite_setOf_absNorm_le₀

Modification history

2026-07-17 09:57

Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

chore(Data): rename `setOf` to `Set.ofPred` (#41507) …

Deleted Ideal.finite_setOf_absNorm_le₀ View on Github →

2025-05-07 16:46

Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

feat(NumberField/Ideal): asymptotics for the number of integral ideals of bounded norm (#22866) …

Added Ideal.finite_setOf_absNorm_le₀ View on Github →