Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-09 07:29 4efa9d8a

View on Github →

chore(algebra/direct_limit): remove module.directed_system (#10636) This typeclass duplicated _root_.directed_system

Estimated changes

Modified src/algebra/category/Module/limits.lean

Modified src/algebra/direct_limit.lean

deleted theorem module.direct_limit.totalize_apply

added theorem module.direct_limit.totalize_of_le

added theorem module.direct_limit.totalize_of_not_le

added theorem module.directed_system.map_map

added theorem module.directed_system.map_self