instMonoFShortComplexTruncLE

Mathlib.Algebra.Homology.Embedding.TruncLEHomology

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.instMonoFShortComplexTruncLE

English

The short complex obtained from K via shortComplexTruncLE e is short exact.

Русский

Полученная короткая последовательность из K через shortComplexTruncLE e является коротко точной.

LaTeX

$$$ (K.shortComplexTruncLE e).ShortExact $$$

Lean4

instance : Mono (K.shortComplexTruncLE e).f :=
  by
  dsimp [shortComplexTruncLE]
  infer_instance

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

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

Разделы

Аффилиация

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