Commit 2024-03-15 09:45 6f69c4d3

View on Github →

refactor: flip LinearMap.convexHull_image and rename to LinearMap.image_convexHull (#11298)

  • flip LinearMap.convexHull_image and rename to image_convexHull
  • while at it, also flip the direction of convexHull_smul and convexHull_neg to match this
  • fix argument order of AffineMap.convexHull_image: have the AffineMap argument come first; there's no good reason not to and this enables dot notation
  • inline variable (s : Set E) to achieve this; this is slightly clearer anyway zulip discussion

Estimated changes

modified theorem AffineMap.image_convexHull
modified theorem affineSpan_convexHull
modified theorem convexHull_neg
modified theorem convexHull_smul