feat(RingTheory/Ideal/Height): add trivial case (leanprover-community#27705)

Update `RingTheory.Ideal.Height`, which adds a simple lemma `Ideal.height_of_subsingleton`. It computes the height of (any) ideal in a zero commutative ring.

Author: yonggyuchoimath

Mathlib/RingTheory/Ideal/Height.lean

@@ -169,6 +169,11 @@ lemma Ideal.primeHeight_eq_zero_iff {I : Ideal R} [I.IsPrime] :
   · rintro ⟨hI, hI'⟩ b hb
     exact hI' (y := b.asIdeal) b.isPrime hb
 
+/-- In a trivial commutative ring, the height of any ideal is `∞`. -/
+@[simp, nontriviality]
+lemma Ideal.height_of_subsingleton [Subsingleton R] : I.height = ⊤ := by
+  rw [Subsingleton.elim I ⊤, Ideal.height_top]
+
 theorem Ideal.isMaximal_of_primeHeight_eq_ringKrullDim {I : Ideal R} [I.IsPrime]
     [FiniteRingKrullDim R] (e : I.primeHeight = ringKrullDim R) : I.IsMaximal := by
   have h : I ≠ ⊤ := by