mathlib documentation

algebraic_topology.fundamental_groupoid.punit

Fundamental groupoid of punit #

The fundamental groupoid of punit is naturally isomorphic to category_theory.discrete punit

@[protected, instance]