lsmul_flip_apply — Mathlib

English

Multiplication by a scalar intertwines with span operations; hence the span of a vector is mapped to the span of the scalar multiple.

Русский

Умножение на скаляр взаимно согласовано с операциями над областью (span); образ линейной комбинации соответствует области скаляра.

LaTeX

$$$\mathrm{toSpanSingleton}\; (c\cdot x) = c\cdot \mathrm{toSpanSingleton}\; x$$$

Lean4

@[simp]
theorem lsmul_flip_apply (x : E) : (lsmul 𝕜 𝕜).flip x = toSpanSingleton 𝕜 x :=
  rfl

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