English
The matrix formed by barycentric coordinates from a basis to another is a unit, hence invertible with inverse given by the reverse change of basis.
Русский
Матрица, образованная барицентрическими координатами между базисами, является обратимой; существует обратная матрица, соответствующая обратному переходу базиса.
LaTeX
$$IsUnit(b.toMatrix p) with the inverse given by b₂.toMatrix b.$$
Lean4
theorem isUnit_toMatrix_iff [Nontrivial k] (p : ι → P) :
IsUnit (b.toMatrix p) ↔ AffineIndependent k p ∧ affineSpan k (range p) = ⊤ :=
by
constructor
· rintro ⟨⟨B, A, hA, hA'⟩, rfl : B = b.toMatrix p⟩
exact ⟨b.affineIndependent_of_toMatrix_right_inv p hA, b.affineSpan_eq_top_of_toMatrix_left_inv p hA'⟩
· rintro ⟨h_tot, h_ind⟩
let b' : AffineBasis ι k P := ⟨p, h_tot, h_ind⟩
change IsUnit (b.toMatrix b')
exact b.isUnit_toMatrix b'
