Theorem Ideal.absNorm_of_ne_bot

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_of_ne_bot View on Github →