hasInjectiveDimensionLT_zero — Mathlib

English

If X is zero, then HasInjectiveDimensionLT X 0 holds.

Русский

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

LaTeX

$$$\text{HasInjectiveDimensionLT}(X,0)$$$

Lean4

theorem hasInjectiveDimensionLT_zero (hX : IsZero X) : HasInjectiveDimensionLT X 0 :=
  by
  letI := HasExt.standard C
  rw [hasInjectiveDimensionLT_iff]
  intro i hi Y e
  rw [← e.comp_mk₀_id, hX.eq_zero_of_tgt (𝟙 X), Ext.mk₀_zero, Ext.comp_zero]

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