Theorem ringKrullDim_eq_bot_iff_subsingleton

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