toMatrix — Mathlib

English

For an affine basis b and a family of points q, the matrix with rows given by barycentric coordinates of q relative to b is defined.

Русский

Для аффинной базы b и семейства точек q матрица с строками, заданными барицентрическими координатами q относительно b, определена.

LaTeX

$$$(b.toMatrix\\ q)_{i j} = b.coord j (q i).$$$

Lean4

/-- 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`. -/
noncomputable def toMatrix {ι' : Type*} (q : ι' → P) : Matrix ι' ι k := fun i j => b.coord j (q i)

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