shift_units_smul — Mathlib

English

Compatibility of rightUnshift with composition of cochains: (γ1 γ2).rightUnshift with composition equals composition of rightUnshifted parts with a shifted target, up to a sign depending on a.

Русский

Совместимость rightUnshift с композиционным произведением: (γ1 γ2).rightUnshift равняется композиции правых Unshift-образов с сдвигом цели, с возможной знаковой модификацией.

LaTeX

$$$((\gamma_1 \circ \gamma_2).rightUnshift nm' hnm') = \text{(смещённая композиция)}$$$

Lean4

@[simp]
theorem shift_units_smul (a : ℤ) (x : Rˣ) : (x • γ).shift a = x • (γ.shift a) :=
  by
  ext p q hpq
  dsimp
  simp only [shift_v', units_smul_v]

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