basisAux_map_smul — Mathlib

English

The basis maps basis elements to simple tensors: the i-th basis vector corresponds to 1 ⊗M basis coefficient at i.

Русский

Устойчивое отображение базиса отправляет i-ую базисную вектору в тензор 1 ⊗ b_i.

LaTeX

$$$basis A b\, i = 1 ⊗M b_i$$$

Lean4

theorem basisAux_map_smul (a : A) (x : A ⊗[R] M) : basisAux A b (a • x) = a • basisAux A b x :=
  TensorProduct.induction_on x (by simp) (fun x y => by simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc])
    fun x y hx hy => by simp [hx, hy]

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