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.

Estimated changes