isNoetherianObject_of_isZero — Mathlib

English

If X is a zero object, then X is Noetherian.

Русский

Если X является нулевым объектом, то X — нётерановский.

LaTeX

$$$\text{IsZero}(X) \Rightarrow \text{IsNoetherianObject}(X).$$$

Lean4

theorem isNoetherianObject_of_isZero (hX : IsZero X) : IsNoetherianObject X :=
  by
  rw [isNoetherianObject_iff_monotone_chain_condition]
  have := Subobject.subsingleton_of_isZero hX
  intro f
  exact ⟨0, fun m hm ↦ Subsingleton.elim _ _⟩

Похожие утверждения