Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
Hi @erikmd @proux01, is there any news on the `mathcomp/mathcomp:2.4.0-coq-8.19` image? It's not there yet.
@erikmd Don't worry. I was just wondering whether I should remove it from a CI config for the moment, and it's not a critical issue for me. Thanks a lot...
How do you plan to make a lemma `lem` in ssralg available as `GRing.lem` and exported from `GRing.Theory`?
@CohenCyril Shouldn't we postpone this to 2.5.0?
I'm self-requesting a review since I need to understand this PR to review the overlay PRs, but I may not have time to do that very soon. By when do...
I rebenched on coq-master: ``` After | Peak Mem | File Name | Before | Peak Mem || Change || Change (mem) | % Change | % Change (mem) -------------------------------------------------------------------------------------------------------------------------------------------...
Speaking of the namespaces like `GRing` and the prefixes like `g` and `r`, given that `monoid.v` and `comoid.v` would provide a common interface between `fingroup` and `ssralg` that cannot be...
FTR, I noticed that this PR would allow us to unify the definitions of multiplication and multiplicative functions for semirings and monomials (in multinomials).
@Tragicus Can you rebase this PR again? Then I can review (at least double-check that all the comments above are addressed).
Other comments: - The naming inconsistencies of the `_closed` constants and lemmas in `comoid.v` and `ssralg.v` should be discussed in the MathComp meeting. - Some part of the header documentation...