grhkm21
grhkm21
Sorry for the long wait, exams :( Fixed the issues above!
I have reverted the `ite` -> `if-then-else` changes (TIL about `git reset --patch`). Hope it's okay now :D
Okay I should have cleaned up stuff. Also I realised a proof didn't even compile, so I fixed that (it depended on the `prod_ite_eq_iff` thing
Sorry, my browser automatically corrects wikipedia links to wikiwand.
@jcommelin Done, sorry about that
@b-mehta do you mind reviewing the latest (two) commits? I added the nat versions as suggested
can you rebase so that CI can run? I can do a final review after that.
Is this ready for review?
I'm not familiar with #36380, but if it does affect this PR someone will tell us.
> I think you'll be better off with making a class for arbitrary finite `ZZ`-linear combinations of the morphisms, not just sums. Then you can implement not just `_add_` but...