Theorem Ideal.finite_setOfPred_absNorm_le₀

Modification history

2026-08-15 05:01

Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

chore(RingTheory/Ideal/Norm): move the `cardQuot` finiteness API into `AbsNorm` (#42784) …

Modified Ideal.finite_setOfPred_absNorm_le₀ View on Github →

2026-07-17 09:57

Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

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

Added Ideal.finite_setOfPred_absNorm_le₀ View on Github →