mathlib
bd1fc183 - refactor(linear_algebra/affine_space/affine_{map,equiv}): add fun_like instances (#18575)

Commit
2 years ago
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.
Author
Parents
Loading