Mathlib v3 is deprecated. Go to Mathlib v4

Theorem module.direct_limit.totalize_of_le

Modification history

2021-12-09 07:29
src/algebra/direct_limit.lean
chore(algebra/direct_limit): remove module.directed_system (#10636) …
Added module.direct_limit.totalize_of_leView on Github →