Commit 2026-08-12 12:06 8bc9575d

View on Github →

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

Estimated changes

Modified Mathlib/Order/WithBot.lean

added theorem WithBot.coe_bot_le

Modified Mathlib/RingTheory/KrullDimension/Basic.lean

added theorem ringKrullDim_eq_bot_iff_subsingleton

modified theorem ringKrullDim_eq_bot_of_subsingleton

modified theorem ringKrullDim_nonneg_of_nontrivial

added theorem zero_le_ringKrullDim_iff_nontrivial