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 src/algebra/direct_limit.lean

modified def add_comm_group.direct_limit.lift

deleted theorem add_comm_group.direct_limit.lift_add

deleted theorem add_comm_group.direct_limit.lift_neg

deleted theorem add_comm_group.direct_limit.lift_sub

modified theorem add_comm_group.direct_limit.lift_unique

deleted theorem add_comm_group.direct_limit.lift_zero

modified theorem add_comm_group.direct_limit.of.zero_exact

modified def add_comm_group.direct_limit.of

deleted theorem add_comm_group.direct_limit.of_add

deleted theorem add_comm_group.direct_limit.of_neg

deleted theorem add_comm_group.direct_limit.of_sub

deleted theorem add_comm_group.direct_limit.of_zero

modified def add_comm_group.direct_limit

modified def ring.direct_limit.lift

deleted theorem ring.direct_limit.lift_add

deleted def ring.direct_limit.lift_hom

deleted theorem ring.direct_limit.lift_mul

deleted theorem ring.direct_limit.lift_neg

deleted theorem ring.direct_limit.lift_one

deleted theorem ring.direct_limit.lift_pow

deleted theorem ring.direct_limit.lift_sub

modified theorem ring.direct_limit.lift_unique

deleted theorem ring.direct_limit.lift_zero

modified theorem ring.direct_limit.of.zero_exact

modified def ring.direct_limit.of

deleted theorem ring.direct_limit.of_add

modified theorem ring.direct_limit.of_injective

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

modified theorem ring.direct_limit.polynomial.exists_of