rightShift_leftShift — Mathlib

English

Analogously to the previous result, performing a left shift followed by a right shift yields the same as shifting γ by a, up to the same sign factor depending on a and n'.

Русский

Аналогично предыдущему результату, выполнение левого сдвига, затем правого, эквивалентно сдвигу γ на a, с тем же фактором знака, зависящим от a и n'.

LaTeX

$$$ (\gamma^{\mathrm{leftShift}}(a,n',hn'))^{\mathrm{rightShift}}(a,n,hn') = (-1)^{a\,n' + \frac{a(a-1)}{2}} \; \gamma^{\mathrm{shift}}(a). $$$

Lean4

theorem rightShift_leftShift (a n' : ℤ) (hn' : n + a = n') :
    (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + (a * (a - 1)) / 2).negOnePow • γ.shift a :=
  by
  ext p q hpq
  simp only [rightShift_v _ a n hn' p q hpq (q + a) (by cutsat),
    leftShift_v _ a n' hn' p (q + a) (by cutsat) (p + a) (by cutsat), units_smul_v, shift_v']
  dsimp
  rw [id_comp, comp_id]

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