Def add_comm_group.direct_limit.of

Modification history

2020-11-12 16:36

src/algebra/direct_limit.lean

chore(algebra/direct_limit): Use bundled morphisms (#4964) …

Modified add_comm_group.direct_limit.of View on Github →

2019-06-16 19:28

src/algebra/direct_limit.lean

Direct limit of modules, abelian groups, rings, and fields. (#754) …

Added add_comm_group.direct_limit.of View on Github →