Commit 2020-11-12 16:36 97a7f577

View on Github →

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

Estimated changes

modified def ring.direct_limit.of
deleted theorem ring.direct_limit.of_add
deleted theorem ring.direct_limit.of_mul
deleted theorem ring.direct_limit.of_neg
deleted theorem ring.direct_limit.of_one
deleted theorem ring.direct_limit.of_pow
deleted theorem ring.direct_limit.of_sub
deleted theorem ring.direct_limit.of_zero