Commit 2021-10-11 04:03 c02a6559

View on Github →

feat(linear_algebra/affine_space/barycentric_coords): we can recover a point from its barycentric coordinates (#9629) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/linear_algebra/affine_space/barycentric_coords.lean

added theorem affine_combination_barycentric_coord_eq_self

added theorem sum_barycentric_coord_apply_eq_one

Modified src/linear_algebra/affine_space/combination.lean

added theorem eq_affine_combination_of_mem_affine_span_of_fintype