Commit 2021-11-23 20:50 eb8b1b82

View on Github →

feat(linear_algebra/affine_space/barycentric_coords): characterise affine bases in terms of coordinate matrices (#10370) Formalized as part of the Sphere Eversion project.

Estimated changes

Modified src/linear_algebra/affine_space/barycentric_coords.lean

added theorem affine_basis.affine_independent_of_to_matrix_right_inv

added theorem affine_basis.affine_span_eq_top_of_to_matrix_left_inv

added theorem affine_basis.ext_elem

added theorem affine_basis.is_unit_to_matrix_iff

added theorem affine_basis.to_matrix_row_sum_one

Modified src/linear_algebra/affine_space/independent.lean

added theorem affine_independent_iff_eq_of_fintype_affine_combination_eq