mathlib
8195826f - refactor(category theory/cofiltered_systems): rename `mittag_leffler.lean` and move `nonempty_sections_of_fintype_cofiltered_system` into new file (#18433)

Commit
2 years ago
refactor(category theory/cofiltered_systems): rename `mittag_leffler.lean` and move `nonempty_sections_of_fintype_cofiltered_system` into new file (#18433) * Create new file `category_theory/cofiltered_system.lean`. * Delete `category_theory/mittag_leffler.lean` and move its content there. * Move `nonempty_sections_of_fintype_cofiltered_system` and `nonempty_sections_of_fintype_inverse_system` there. * Some new lemmas. Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Author
Parents
Loading