mathlib3 documentation


Profinite sets have enough projectives #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we show that Profinite has enough projectives.

Main results #

Let X be a profinite set.

For any profinite X, the natural map ultrafilter X → X is a projective presentation.