shiftFunctorComm_eq — Mathlib

English

For i, j, k ∈ A with i+j=k, the shiftFunctorComm C i j is equal to the composition of the inverse/additive structure shiftFunctorAdd' between i and j and its symmetric counterpart.

Русский

Для i, j, k ∈ A с i+j=k, shiftFunctorComm C i j равен композиции обратной копии и структуры сложения между i и j и её симметричного аналога.

LaTeX

$$$ \\ shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm \\ gg shiftFunctorAdd' C j i k (by rw [add_comm j i, h]) $$$

Lean4

theorem shiftFunctorComm_eq (i j k : A) (h : i + j = k) :
    shiftFunctorComm C i j = (shiftFunctorAdd' C i j k h).symm ≪≫ shiftFunctorAdd' C j i k (by rw [add_comm j i, h]) :=
  by
  subst h
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd]
  rfl

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