leftShift_units_smul — Mathlib

English

There is a linear equivalence between Cochain K L n and Cochain (K⟦a⟧) (L) n' for hn, built from leftShiftAddEquiv and a smul-adjusted map.

Русский

Существует линейное эквивалентное отображение между Cochain K L n и Cochain (K⟦a⟧) L n' при hn, построенное на основе leftShiftAddEquiv и шкалируемой карты.

LaTeX

$$$\text{leftShiftLinearEquiv}(n,a,n',hn) : Cochain K L n \simeq_{\text{linear}} Cochain (K⟦a⟧) L n'$$$

Lean4

@[simp]
theorem leftShift_units_smul (a n' : ℤ) (hn' : n + a = n') (x : Rˣ) :
    (x • γ).leftShift a n' hn' = x • γ.leftShift a n' hn' := by apply leftShift_smul

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