Theorem Ideal.finite_setOfPred_absNorm_le₀

Modification history

2026-10-27 14:08

Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

refactor(RingTheory/Ideal/Norm/AbsNorm): state the absNorm finiteness lemmas for rings with finite quotients (#45255) …

Deleted Ideal.finite_setOfPred_absNorm_le₀ View on Github →

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 →