Commit 2025-04-07 02:11 2f184a42
View on Github →feat(Analysis/Normed/Affine/ContinuousAffineMap): affine space instance (#23735)
Add an instance for continuous affine maps as an affine space, analogous to one that already exists for plain AffineMap. (The apply lemmas are simp lemmas since the corresponding AffineMap ones are.)