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]