toMatrix_inv_vecMul_toMatrix — Mathlib

English

If the barycentric matrices relative to two bases are invertible, then applying the inverse recovers the coordinates in the second basis.

Русский

Если матрицы барицентрических координат двух баз взаимно обращимы, то применение обратной матрицы восстанавливает координаты во второй базе.

LaTeX

$$$\\mathbf{coords}(x) \\; ᵥ*\\; (b.toMatrix b_2)^{-1} = b_2.coords(x).$$$

Lean4

/-- A change of basis formula for barycentric coordinates.

See also `AffineBasis.toMatrix_vecMul_coords`. -/
@[simp]
theorem toMatrix_inv_vecMul_toMatrix (x : P) : b.coords x ᵥ* (b.toMatrix b₂)⁻¹ = b₂.coords x :=
  by
  have hu := b.isUnit_toMatrix b₂
  rw [Matrix.isUnit_iff_isUnit_det] at hu
  rw [← b.toMatrix_vecMul_coords b₂, Matrix.vecMul_vecMul, Matrix.mul_nonsing_inv _ hu, Matrix.vecMul_one]

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