Commit 2023-03-13 22:49 bd1fc183
View on Github →refactor(linear_algebra/affine_space/affine_{map,equiv}): add fun_like instances (#18575)
Going all the way and defining a new affine_map_class class can wait till after the port; but adding fun_like makes the port easier.
This has to reorder a few declarations in affine_equiv.lean.
The only new declarations are the new instances.