units_smul_comp — Mathlib

English

Let k be a unit in the ring R, and let z1, z2 be cochains of degrees n1 and n2 respectively with n1 + n2 = n12. Then the action of k on z1 commutes with composition: (k • z1) ∘ z2 = k • (z1 ∘ z2).

Русский

Пусть k — единица кольца R, z1 и z2 — коцепи степеней n1 и n2 соответственно с n1 + n2 = n12. Тогда действие k на z1 commute с композицией: (k • z1) ∘ z2 = k • (z1 ∘ z2).

LaTeX

$$$\\\\forall k \\\\in R^{\\\\times}, \\\\forall z_1 \\\\in Cochain F G n_1, \\\\forall z_2 \\\\in Cochain G K n_2, \\\\forall h: n_1+n_2=n_{12}, \\\\ (k \\\\cdot z_1) \\\\circ z_2 \, h \;=\\; k \\\\cdot (z_1 \\\\circ z_2 \, h).$$$

Lean4

@[simp]
theorem units_smul_comp {n₁ n₂ n₁₂ : ℤ} (k : Rˣ) (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (h : n₁ + n₂ = n₁₂) :
    (k • z₁).comp z₂ h = k • (z₁.comp z₂ h) := by apply Cochain.smul_comp

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