Theorem Convexity.ConvexSpace.AffineMap.comp_id

Modification history

2026-09-11 16:02
Mathlib/Geometry/Convex/ConvexSpace/AffineMap.lean
feat(Geometry/Convex): affine maps into a module form a module (#43586) …
Modified Convexity.ConvexSpace.AffineMap.comp_idView on Github →
2026-07-28 04:48
Mathlib/Geometry/Convex/ConvexSpace/AffineMap.lean
feat(Geometry/Convex): bundled type of affine maps between convex spaces (#42126)
Added Convexity.ConvexSpace.AffineMap.comp_idView on Github →