mathlib
fd783e39 - chore(algebra/free_algebra): remove a heavy and unecessary import (#10093)

Commit

4 years ago

chore(algebra/free_algebra): remove a heavy and unecessary import (#10093) `transfer_instance` pulls in category theory, which is overkill

Author

eric-wieser

Parents