Commit 2023-02-01 09:29 2f4cdce0
View on Github →feat(linear_algebra/affine_space/basis): reindex
API (#18190)
Rename and change arguments to affine_basis.comp_equiv
so that it matches basis.reindex
. Provide lemmas for its interaction with other affine_basis
constructions.
Make affine_basis
follow the fun_like
design, replacing affine_basis.points
by a function coercion.
Fix a few names all around:
affine_basis.coord_apply_neq
→affine_basis.coord_apply_ne
convex_hull_affine_basis_eq_nonneg_barycentric
→affine_basis.convex_hull_eq_nonneg_coord