units_smul_v — Mathlib

English

Multiplication by a unit behaves the same on the v-component as multiplication by a scalar.

Русский

Умножение на единицу ведёт себя на компоненте v так же, как и скалярное умножение.

LaTeX

$$$ (k \\cdot z).v(p,q;hpq) = k \\cdot (z.v(p,q;hpq)) $ for k \\in R^×$$

Lean4

@[simp]
theorem units_smul_v {n : ℤ} (k : Rˣ) (z : Cochain F G n) (p q : ℤ) (hpq : p + n = q) :
    (k • z).v p q hpq = k • (z.v p q hpq) :=
  rfl

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