leftUnshift_units_smul — Mathlib

English

For γ, a, and a unit x, the rightUnshift respects smul with units: (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn.

Русский

Для γ, a и единиц x: rightUnshift сохраняет умножение на единицы: (x • γ).rightUnshift n hn = x • γ.rightUnshift n hn.

LaTeX

$$$(x \cdot γ).rightUnshift n hn = x \cdot (γ.rightUnshift n hn)$$$

Lean4

@[simp]
theorem leftUnshift_units_smul {n' a : ℤ} (γ : Cochain (K⟦a⟧) L n') (n : ℤ) (hn : n + a = n') (x : Rˣ) :
    (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn := by apply leftUnshift_smul

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