Theorem Ideal.absNorm_eq_natCard

Modification history

2026-10-17 09:16

Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

refactor(RingTheory/Ideal/Norm): give `Ideal.absNorm` the junk value `0` at `⊥` (#44698) …

Added Ideal.absNorm_eq_natCard View on Github →