det_smul_coords_eq_cramer_coords — Mathlib

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]

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