truncGEMap_id

Mathlib.Algebra.Homology.Embedding.TruncGE

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

English

TruncGEMap of the identity on K is the identity on K.truncGE(e).

Русский

TruncGEMap тождественного отображения на K равен тождественному отображению на K.truncGE(e).

LaTeX

$$$truncGEMap(\mathrm{id}_K, e) = \mathrm{id}_{K.truncGE(e)}$$$

Lean4

@[simp]
theorem truncGEMap_id : truncGEMap (𝟙 K) e = 𝟙 _ := by simp [truncGEMap, truncGE]

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

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

Разделы

Аффилиация

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