Commit 2025-07-19 04:00 775b8cc7

View on Github →

feat(Topology/Algebra/ContinuousAffineMap): define id (#27259) This is was some missing API

Estimated changes

Modified Mathlib/Topology/Algebra/ContinuousAffineMap.lean

modified theorem ContinuousAffineMap.coe_comp

modified theorem ContinuousAffineMap.coe_const

added theorem ContinuousAffineMap.coe_id

modified theorem ContinuousAffineMap.comp_apply

added theorem ContinuousAffineMap.comp_id

added def ContinuousAffineMap.id

added theorem ContinuousAffineMap.id_comp