Def FundamentalGroupoid.punitEquivDiscretePunit

Modification history

2023-06-09 07:23
Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean
chore: review of automation in category theory (#4793) …
Deleted FundamentalGroupoid.punitEquivDiscretePunitView on Github →
2023-05-18 08:20
Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean
feat: port AlgebraicTopology.FundamentalGroupoid.Punit (#4053)
Added FundamentalGroupoid.punitEquivDiscretePunitView on Github →