shiftFunctor₁XXIso_refl

Mathlib.Algebra.Homology.TotalComplexShift

URI: https://scilib.ai/kg/mathlib#HomologicalComplex₂.shiftFunctor₁XXIso_refl

English

The identity case of the Shift1XXIso: shifting by zero yields a trivial isomorphism (identity).

Русский

Случай тождества в Shift1XXIso: сдвиг на ноль даёт тривиальный изоморфизм (тождественный).

LaTeX

$$$K.shiftFunctor1XXIso a x (a+x) rfl b = Iso.refl _.$$$

Lean4

@[simp]
theorem shiftFunctor₁XXIso_refl (a b x : ℤ) : K.shiftFunctor₁XXIso a x (a + x) rfl b = Iso.refl _ :=
  rfl

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

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

Разделы

Аффилиация

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