HasProjectiveDimensionLE — Mathlib

English

HasProjectiveDimensionLE(X,n) is the same as HasProjectiveDimensionLT(X,n+1).

Русский

HasProjectiveDimensionLE(X,n) эквивалентно HasProjectiveDimensionLT(X,n+1).

LaTeX

$$$ \operatorname{HasProjectiveDimensionLE}(X,n) \equiv \operatorname{HasProjectiveDimensionLT}(X,n+1) $$$

Lean4

/-- An object `X` in an abelian category has projective dimension `≤ n` if
all `Ext X Y i` vanish when `n + 1 ≤ i` -/
abbrev HasProjectiveDimensionLE (X : C) (n : ℕ) : Prop :=
  HasProjectiveDimensionLT X (n + 1)

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