Commit 2025-04-25 00:52 c2e31189

feat(LinearAlgebra/AffineSpace/ContinuousAffineEquiv): toContinuousAffineMap (#23732) Add the conversion from ContinuousAffineEquiv to ContinuousAffineMap, which seems to be missing from mathlib. I'm not sure exactly what API such conversions are meant to have - toHomeomorph doesn't have any - but I added rfl lemmas about converting to a function either directly or via toContinuousAffineMap, and about different pairs of conversion paths involving toContinuousAffineMap producing the same result, as well as injectivity of toContinuousAffineMap.