smul_mat_cons — Mathlib

English

Let α be a NonUnitalNonAssocSemiring. Then x • vecCons v A = vecCons (x • v) (x • A).

Русский

Пусть α — неединичное неассоциативное полукольцо. Тогда x • vecCons v A = vecCons (x • v) (x • A).

LaTeX

$$$x \cdot \mathrm{vecCons}(v,A) = \mathrm{vecCons}(x\cdot v, x\cdot A)$$$

Lean4

theorem smul_mat_cons (x : α) (v : n' → α) (A : Fin m → n' → α) : x • vecCons v A = vecCons (x • v) (x • A) :=
  by
  ext i
  refine Fin.cases ?_ ?_ i <;> simp

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