basisOf_smul — Mathlib

English

For any a in G, the coordinates of the scaled basis satisfy (a • b).basisOf i = a • b.basisOf i.

Русский

Для любого a ∈ G координаты масштабированного базиса удовлетворяют (a • b).basisOf i = a • b.basisOf i.

LaTeX

$$$ (a \\cdot b).basisOf i = a \\cdot b.basisOf i$$$

Lean4

@[simp]
theorem basisOf_smul (a : G) (b : AffineBasis ι k V) (i : ι) : (a • b).basisOf i = a • b.basisOf i := by ext j;
  simp [smul_sub]

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