Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-02 04:58 37f43bff

View on Github →

feat(linear_algebra/affine_space/barycentric_coords): define barycentric coordinates (#9472)

Estimated changes

Created src/linear_algebra/affine_space/barycentric_coords.lean

added theorem barycentric_coord_apply

added theorem barycentric_coord_apply_combination

added theorem barycentric_coord_apply_eq

added theorem barycentric_coord_apply_neq

added theorem basis_of_aff_ind_span_eq_top_apply

Modified src/linear_algebra/affine_space/basic.lean

Modified src/linear_algebra/basis.lean

added theorem basis.coe_sum_coords

added theorem basis.coe_sum_coords_eq_finsum

added theorem basis.coe_sum_coords_of_fintype

modified def basis.coord

added theorem basis.sum_coords_self_apply