Theorem WithBot.coe_bot_le

Modification history

2026-08-12 12:06
Mathlib/Order/WithBot.lean
feat(RingTheory): a ring is nontrivial iff it has nontrivial Krull dimension (#41074)
Added WithBot.coe_bot_leView on Github →