empty_vecMulVec — Mathlib

English

Let α be a nonunital nonassoc semiring. For v : Fin 0 → α and w : n' → α, we have vecMulVec v w = vecEmpty.

Русский

Пусть α — неединичное неассоциативное полукольцо. Пусть v — пустой вектор из Fin 0, а w — любой вектор, тогда vecMulVec v w = vecEmpty.

LaTeX

$$$\mathrm{vecMulVec}(v,w) = \mathrm{vecEmpty}$ for $v: \mathrm{Fin} 0 \to \alpha$, $w: n' \to \alpha$.$$

Lean4

@[simp]
theorem empty_vecMulVec (v : Fin 0 → α) (w : n' → α) : vecMulVec v w = ![] :=
  empty_eq _

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