rightUnshift_zero — Mathlib

English

Another articulation of the additive equivalence between Cochain K L n and Cochain (K⟦a⟧) L n' for n + a = n', emphasizing the additive structure.

Русский

Ещё одно оформление аддитивной эквивалентности между Cochain(K,L,n) и Cochain(K⟦a⟧,L,n') при n + a = n'.

LaTeX

$$$\\text{leftShiftAddEquiv}(n,a,n',hn'):\\; \\text{Cochain}(K,L,n) \\simeq_+ \\text{Cochain}(K⟦a⟧,L,n')$$$

Lean4

@[simp]
theorem rightUnshift_zero (a n' : ℤ) (hn' : n' + a = n) : (0 : Cochain K (L⟦a⟧) n').rightUnshift n hn' = 0 :=
  by
  change (rightShiftAddEquiv K L n a n' hn').symm 0 = 0
  apply map_zero

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