leftUnshift_leftShift — Mathlib

English

The leftShift and leftUnshift operations commute in the sense that leftShift leftUnshift equals the identity under the right degree condition.

Русский

Операции leftShift и leftUnshift коммутируют: leftShift после leftUnshift равняется тождественному отображению при подходящем условии степеней.

LaTeX

$$$\\text{leftShiftLeftUnshift}(a,n') : ( \\text{leftUnshift }(a,n') ) \\circ ( \\text{leftShift }(a,n') ) = \\mathrm{id}$$$

Lean4

@[simp]
theorem leftUnshift_leftShift (a n' : ℤ) (hn' : n + a = n') : (γ.leftShift a n' hn').leftUnshift n hn' = γ :=
  by
  ext p q hpq
  rw [(γ.leftShift a n' hn').leftUnshift_v n hn' p q hpq (q - n') (by cutsat),
    γ.leftShift_v a n' hn' (q - n') q (by cutsat) p hpq, Linear.comp_units_smul, Iso.inv_hom_id_assoc, smul_smul,
    Int.units_mul_self, one_smul]

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