Mathlib v3 is deprecated. Go to Mathlib v4

Theorem add_comm_group.direct_limit.directed_system

Modification history

2020-10-05 07:39
src/algebra/direct_limit.lean
chore(algebra/direct_limit): linting (#4411)
Deleted add_comm_group.direct_limit.directed_systemView on Github →
2020-03-23 01:05
src/algebra/direct_limit.lean
feat(algebra/module): `f : E →+ F` is `ℚ`-linear (#2215) …
Modified add_comm_group.direct_limit.directed_systemView on Github →
2019-09-22 04:34
src/algebra/direct_limit.lean
chore(*): fix various issues reported by `sanity_check_mathlib` (#1469) …
Added add_comm_group.direct_limit.directed_systemView on Github →