Theorem Ideal.absNorm_ne_zero_iff

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) …

Modified Ideal.absNorm_ne_zero_iff View on Github →

2023-06-22 06:58

Mathlib/RingTheory/Ideal/Norm.lean

feat: port RingTheory.Ideal.Norm (#5311)

Added Ideal.absNorm_ne_zero_iff View on Github →