Zulip Chat Archive

Stream: maths

Topic: AlgebraicTopology.FundamentalGroupoid.Product

Yury G. Kudryashov (Jul 03 2023 at 21:26):

I started porting AlgebraicTopology.FundamentalGroupoid.Product in #5696. The first issue is that Lean fails to generate instances, probably because of the changes in reducibility somewhere.

Yury G. Kudryashov (Jul 03 2023 at 21:38):

And I have similar issues in #5697

Last updated: Dec 20 2023 at 11:08 UTC