# Documentation

Mathlib.LinearAlgebra.AffineSpace.Matrix

# Matrix results for barycentric co-ordinates #

Results about the matrix of barycentric co-ordinates for a family of points in an affine space, with respect to some affine basis.

noncomputable def AffineBasis.toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} (q : ι'P) :
Matrix ι' ι k

Given an affine basis p, and a family of points q : ι' → P, this is the matrix whose rows are the barycentric coordinates of q with respect to p.

It is an affine equivalent of Basis.toMatrix.

Instances For
@[simp]
theorem AffineBasis.toMatrix_apply {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} (q : ι'P) (i : ι') (j : ι) :
= ↑() (q i)
@[simp]
theorem AffineBasis.toMatrix_self {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] :
= 1
theorem AffineBasis.toMatrix_row_sum_one {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] {ι' : Type u_2} (q : ι'P) (i : ι') :
(Finset.sum Finset.univ fun j => ) = 1
theorem AffineBasis.affineIndependent_of_toMatrix_right_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [Fintype ι'] [] [] (p : ι'P) {A : Matrix ι ι' k} (hA : = 1) :

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a right inverse, then p is affine independent.

theorem AffineBasis.affineSpan_eq_top_of_toMatrix_left_inv {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) {ι' : Type u_1} [Fintype ι'] [] [] [] (p : ι'P) {A : Matrix ι ι' k} (hA : = 1) :

Given a family of points p : ι' → P and an affine basis b, if the matrix whose rows are the coordinates of p with respect b has a left inverse, then p spans the entire space.

@[simp]
theorem AffineBasis.toMatrix_vecMul_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] (b₂ : AffineBasis ι k P) (x : P) :
Matrix.vecMul (↑() x) () = ↑() x

A change of basis formula for barycentric coordinates.

See also AffineBasis.toMatrix_inv_vecMul_toMatrix.

theorem AffineBasis.toMatrix_mul_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] (b₂ : AffineBasis ι k P) [] :
* = 1
theorem AffineBasis.isUnit_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] (b₂ : AffineBasis ι k P) [] :
theorem AffineBasis.isUnit_toMatrix_iff {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [Ring k] [Module k V] (b : AffineBasis ι k P) [] [] [] (p : ιP) :
@[simp]
theorem AffineBasis.toMatrix_inv_vecMul_toMatrix {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [] [Module k V] [] [] (b : AffineBasis ι k P) (b₂ : AffineBasis ι k P) (x : P) :
Matrix.vecMul (↑() x) ()⁻¹ = ↑() x

A change of basis formula for barycentric coordinates.

See also AffineBasis.toMatrix_vecMul_coords.

theorem AffineBasis.det_smul_coords_eq_cramer_coords {ι : Type u₁} {k : Type u₂} {V : Type u₃} {P : Type u₄} [] [] [] [Module k V] [] [] (b : AffineBasis ι k P) (b₂ : AffineBasis ι k P) (x : P) :
Matrix.det () ↑() x = ↑() (↑() x)

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.