rightShift_zero — Mathlib

English

There is an additive equivalence between Cochain K L n and Cochain (K⟦a⟧) L n' when n + a = n'. It is inverse to rightShiftAddEquiv and preserves addition.

Русский

Существует аддитивная эквивалентность между Cochain(K,L,n) и Cochain(K⟦a⟧,L,n') при n + a = n'. Она обратна RightShiftAddEquiv и сохраняет сложение.

LaTeX

$$$\\text{leftShiftAddEquiv}(n,a,n',hn'):\\; \\text{Cochain}(K,L,n) \\simeq_+ \\text{Cochain}(K⟦a⟧,L,n'),\\; \\gamma \\mapsto \\gamma.leftShift a n' hn',\\; \\text{inv}=\\gamma.leftUnshift n hn',$$$

Lean4

@[simp]
theorem rightShift_zero (a n' : ℤ) (hn' : n' + a = n) : (0 : Cochain K L n).rightShift a n' hn' = 0 :=
  by
  change rightShiftAddEquiv K L n a n' hn' 0 = 0
  apply map_zero

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