English
A change of basis formula for barycentric coordinates: coordinates with respect to b2 can be obtained from coordinates with respect to b using a left multiplication by the appropriate matrix and its inverse.
Русский
Согласование барицентрических координат при смене базы: координаты по b2 получаются из координат по b через умножение на матрицу и её обратную.
LaTeX
$$$b.coords x \\; ᵥ*\\; b.toMatrix b_2 = b_2.coords x.$$$
Lean4
/-- A change of basis formula for barycentric coordinates.
See also `AffineBasis.toMatrix_inv_vecMul_toMatrix`. -/
@[simp]
theorem toMatrix_vecMul_coords (x : P) : b₂.coords x ᵥ* b.toMatrix b₂ = b.coords x :=
by
ext j
change _ = b.coord j x
conv_rhs => rw [← b₂.affineCombination_coord_eq_self x]
rw [Finset.map_affineCombination _ _ _ (b₂.sum_coord_apply_eq_one x)]
simp [Matrix.vecMul, dotProduct, toMatrix_apply, coords]
