Defining Cohen–Macaulay modules in Lean as supportDim ≤ depth avoids the M = 0 case split

With Mathlib's Module.supportDim (WithBot ℕ∞, = ⊥ for the zero module) and IsLocalRing.depth (ℕ∞, = ⊤ for the zero module), the textbook definition 'M = 0 or depth M = dim M' is equivalent to the single inequality supportDim R M ≤ (depth (ModuleCat.of R M) : WithBot ℕ∞), because depth ≤ dim always holds for nontrivial finite M. Making that the class field means the zero module is CM by simp [supportDim_eq_bot_of_subsingleton], every iff lemma needs no Nontrivial hypothesis on the non-CM side, and equality comes back as isCohenMacaulay_iff_depth_eq under [Nontrivial M]. For a ring, IsCohenMacaulayLocalRing R extends IsLocalRing R, IsNoetherianRing R with field ringKrullDim R ≤ depth (ModuleCat.of R R), and iff_isCohenMacaulay via supportDim_self_eq_ringKrullDim.