Theorem zero_le_ringKrullDim_iff_nontrivial

Modification history

2026-08-12 12:06

Mathlib/RingTheory/KrullDimension/Basic.lean

feat(RingTheory): a ring is nontrivial iff it has nontrivial Krull dimension (#41074)

Added zero_le_ringKrullDim_iff_nontrivial View on Github →