!4#3961

Stream: PR reviews

[Matthew Ballard]

There was some duplication of existing API in topology.homotopy.product in !4#2984. I fixed the actual errors but perhaps someone else might have a stronger opinion on the correct homes for results @Yury G. Kudryashov

[Yury G. Kudryashov]

I'm sorry for creating this mess. I should've looked at mathlib3 before adding new definitions. I'll have a look at the PR tonight.

[Matthew Ballard]

No worries. I just want to make sure the people invested get heard.

[Eric Wieser]

This is one of the reasons I was hesitant about contributing "new" content to mathlib4 before the port is over

[Yury G. Kudryashov]

And now I agree with you...