Mathlib Changelog
v3
Changelog
About
Github
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