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_neq → affine_basis.coord_apply_ne
  • convex_hull_affine_basis_eq_nonneg_barycentric → affine_basis.convex_hull_eq_nonneg_coord

Estimated changes

added theorem equiv_like.range_comp
modified theorem set.preimage_injective
modified theorem affine_basis.coord_apply
modified theorem affine_basis.coord_apply_eq
added theorem affine_basis.ext
modified theorem affine_basis.ext_elem
added theorem affine_basis.ind
added theorem affine_basis.tot
deleted theorem basis.coe_reindex_repr
modified theorem basis.eq_of_apply_eq
modified theorem basis.eq_of_repr_eq_repr
deleted theorem basis.range_reindex'
deleted theorem basis.reindex_repr
added theorem basis.repr_injective
added theorem basis.repr_reindex