intCast_mulVec — Mathlib

English

For any x ∈ ℤ and v ∈ m → α, intCast_vecMul asserts x ᵥ* v = (x : α) • v, i.e., left action of integers matches scalar action through embedding.

Русский

Для целого x и вектора v верно x ᵥ* v = (x : α) • v, т. к. целые интегрируются в α и действуют как скалярное умножение.

LaTeX

$$$x ᵥ* v = (x : α) • v$$$

Lean4

@[simp]
theorem intCast_mulVec (x : ℤ) (v : m → α) : x *ᵥ v = (x : α) • v :=
  diagonal_const_mulVec _ _

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