mathlib3
86e93623 - feat(algebraic_topology): the category simplicial_object.split (#16274)

Commit

3 years ago

feat(algebraic_topology): the category simplicial_object.split (#16274) This PR introduces the category of simplicial objects equipped with a splitting.

Author

joelriou

Parents

c82fab81

mathlib3 86e93623 - feat(algebraic_topology): the category simplicial_object.split (#16274)

mathlib3
86e93623 - feat(algebraic_topology): the category simplicial_object.split (#16274)