English
For x ∈ R mapping to K in the fraction field, ordFrac equals ordMonoidWithZeroHom when x comes from R.
Русский
Для x, переходящего из R в K в дробном поле, ordFrac совпадает с ordMonoidWithZeroHom.
LaTeX
$$ordFrac R = ordMonoidWithZeroHom R on images of R in K$$
Lean4
/-- The quotient of a Noetherian ring of krull dimension less than or equal to `1` by a principal ideal
is of finite length.
-/
theorem _root_.isFiniteLength_quotient_span_singleton [IsNoetherianRing R] [Ring.KrullDimLE 1 R] {x : R}
(hx : x ∈ nonZeroDivisors R) : IsFiniteLength R (R ⧸ Ideal.span { x }) :=
by
rw [isFiniteLength_iff_isNoetherian_isArtinian]
suffices IsArtinianRing (R ⧸ Ideal.span { x }) from
⟨isNoetherian_quotient (Ideal.span { x }),
isArtinian_of_surjective_algebraMap (Ideal.Quotient.mk_surjective (I := .span { x }))⟩
rw [isArtinianRing_iff_krullDimLE_zero, Ring.KrullDimLE, Order.krullDimLE_iff, ←
WithBot.add_le_add_iff_right' (c := 1) (by simp) (WithBot.coe_eq_coe.not.mpr (by simp)), Nat.cast_zero, zero_add]
exact (ringKrullDim_quotient_succ_le_of_nonZeroDivisor hx).trans (Order.KrullDimLE.krullDim_le)
