coord_smul — Mathlib

English

The coordinate of a translated basis equals the composition of the original coordinate with the inverse of the translation map.

Русский

Координата перенесённого базиса равна композиции исходной координаты с обратным отображением переноса.

LaTeX

$$$\\forall i,\\; (v +ᵥ b).coord i = (b.coord i) \\circ (AffineEquiv.constVAdd\\ k\\ P\\ v)^{-1}$$$

Lean4

@[simp]
theorem coord_smul (a : G) (b : AffineBasis ι k V) (i : ι) :
    (a • b).coord i = (b.coord i).comp (DistribMulAction.toLinearEquiv _ _ a).symm.toAffineMap := by ext v;
  simp [map_sub, coord]

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