Mathlib v3 is deprecated. Go to Mathlib v4

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_neqaffine_basis.coord_apply_ne
  • convex_hull_affine_basis_eq_nonneg_barycentricaffine_basis.convex_hull_eq_nonneg_coord

Estimated changes