isZero_of_hasProjectiveDimensionLT_zero

English

If HasProjectiveDimensionLT X 0 holds, then X is zero.

Русский

Если HasProjectiveDimensionLT X 0, то X есть нулевой объект.

LaTeX

$$$ [\text{HasProjectiveDimensionLT } X 0] \Rightarrow \text{IsZero } X $$$

Lean4

theorem isZero_of_hasProjectiveDimensionLT_zero [HasProjectiveDimensionLT X 0] : IsZero X :=
  by
  letI := HasExt.standard C
  rw [IsZero.iff_id_eq_zero]
  apply Ext.homEquiv₀.symm.injective
  simpa only [Ext.homEquiv₀_symm_apply, Ext.mk₀_zero] using Abelian.Ext.eq_zero_of_hasProjectiveDimensionLT _ 0 (by rfl)

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