Commit 2026-07-28 04:48 996c0942

View on Github →

feat(Geometry/Convex): bundled type of affine maps between convex spaces (#42126)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Geometry/Convex/ConvexSpace/AffineMap.lean

added theorem Convexity.ConvexSpace.AffineMap.assoc

added theorem Convexity.ConvexSpace.AffineMap.coe_comp

added def Convexity.ConvexSpace.AffineMap.comp

added theorem Convexity.ConvexSpace.AffineMap.comp_id

added def Convexity.ConvexSpace.AffineMap.const

added theorem Convexity.ConvexSpace.AffineMap.ext

added def Convexity.ConvexSpace.AffineMap.id

added theorem Convexity.ConvexSpace.AffineMap.id_comp

added theorem Convexity.ConvexSpace.AffineMap.isAffineMap

Modified Mathlib/Geometry/Convex/ConvexSpace/Defs.lean

added theorem Convexity.IsAffineMap.const