mathlib
97a7f577 - chore(algebra/direct_limit): Use bundled morphisms (#4964)

Commit

5 years ago

chore(algebra/direct_limit): Use bundled morphisms (#4964) This introduced some ugliness in the form of `(λ i j h, f i j h)`, which is a little unfortunate

Author

eric-wieser

Parents

34215fc9

mathlib 97a7f577 - chore(algebra/direct_limit): Use bundled morphisms (#4964)

mathlib
97a7f577 - chore(algebra/direct_limit): Use bundled morphisms (#4964)