mathlib
2f4cdce0 - feat(linear_algebra/affine_space/basis): `reindex` API (#18190)

Commit
2 years ago
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`
Author
Parents
Loading