instRefl — Mathlib

English

The identity equivalence is compatible with shifts; i.e., the diagonal identity is a CommShift equivalence.

Русский

Единичная эквивалентность совместима со сдвигами; диагональная единичная эквивалентность является CommShift.

LaTeX

$$$\\text{Equivalence.refl.CommShift } A$$$

Lean4

/-- The identity equivalence is compatible with shifts.
-/
instance : (Equivalence.refl (C := C)).CommShift A :=
  by
  dsimp [Equivalence.CommShift, refl_toAdjunction]
  infer_instance

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