hasInjectiveDimensionLT_zero_iff_isZero

Mathlib.CategoryTheory.Abelian.Injective.Dimension

URI: https://scilib.ai/kg/mathlib#CategoryTheory.hasInjectiveDimensionLT_zero_iff_isZero

← MathLib Explorer

English

HasInjectiveDimensionLT X 0 is equivalent to IsZero X.

Русский

HasInjectiveDimensionLT X 0 эквивалентно IsZero X.

LaTeX

$$$\text{HasInjectiveDimensionLT}(X,0) \;\Leftrightarrow\; \text{IsZero}(X)$$$

Lean4

theorem hasInjectiveDimensionLT_zero_iff_isZero : HasInjectiveDimensionLT X 0 ↔ IsZero X :=
  ⟨fun _ ↦ isZero_of_hasInjectiveDimensionLT_zero X, fun h ↦ h.hasInjectiveDimensionLT_zero⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru