isZero_of_hasInjectiveDimensionLT_zero

English

If there exists HasInjectiveDimensionLT X 0, then X is zero.

Русский

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

LaTeX

$$$\text{IsZero}(X)$$$

Lean4

theorem isZero_of_hasInjectiveDimensionLT_zero [HasInjectiveDimensionLT 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_hasInjectiveDimensionLT _ 0 (by rfl)

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