English
A determinant–based relation links barycentric coordinates under a fixed basis to the Crámer transpose of coordinates.
Русский
Зависимость барицентрических координат от детерминанта через транспонированную матрицу Крамера.
LaTeX
$$$(b.toMatrix b_2).det \\cdot b_2.coords x = (b.toMatrix b_2)^{T.cramer} \\; (b.coords x).$$$
Lean4
/-- If we fix a background affine basis `b`, then for any other basis `b₂`, we can characterise
the barycentric coordinates provided by `b₂` in terms of determinants relative to `b`. -/
theorem det_smul_coords_eq_cramer_coords (x : P) :
(b.toMatrix b₂).det • b₂.coords x = (b.toMatrix b₂)ᵀ.cramer (b.coords x) :=
by
have hu := b.isUnit_toMatrix b₂
rw [Matrix.isUnit_iff_isUnit_det] at hu
rw [← b.toMatrix_inv_vecMul_toMatrix, Matrix.det_smul_inv_vecMul_eq_cramer_transpose _ _ hu]