Skip to content

Add numZmodType#1520

Merged
CohenCyril merged 7 commits into
math-comp:masterfrom
proux01:numzmodtype
Jan 16, 2026
Merged

Add numZmodType#1520
CohenCyril merged 7 commits into
math-comp:masterfrom
proux01:numzmodtype

Conversation

@proux01

@proux01 proux01 commented Jan 13, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

TODO: ensure #1513 (comment) is addressed (done)

Minimal TODO list
  • added changelog entries with doc/changelog/make-entry.sh
  • added corresponding documentation in the headers
  • tried to abide by the contribution guide
  • this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

@proux01 proux01 mentioned this pull request Jan 14, 2026
Draft
7 tasks
@proux01 proux01 force-pushed the numzmodtype branch 2 times, most recently from c38784b to d15d5e2 Compare January 14, 2026 08:57
proux01
proux01 commented Jan 14, 2026
View reviewed changes

@proux01 proux01 left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Will also need changelog (quite some work) but otherwise seems essentially ready.

Comment thread algebra/num_theory/numdomain.v Outdated
Comment thread algebra/num_theory/orderedzmod.v Outdated
@proux01 proux01 added this to the 2.6.0 milestone Jan 14, 2026
@proux01 proux01 marked this pull request as ready for review January 14, 2026 10:34
@CohenCyril

CohenCyril commented Jan 14, 2026

Copy link
Copy Markdown
Member

Hi, what is the relation between this PR and #1338 ? (And did you notice the items I put in the initial message of #1338?)

@proux01

proux01 commented Jan 14, 2026

Copy link
Copy Markdown
Contributor Author

what is the relation between this PR and #1338 ?

#1338 depends on the current PR (added info to top message there)

did you notice the items I put in the initial message of #1338?

I'd say all these items remain in #1338

@coqbot-app coqbot-app Bot added the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jan 15, 2026
@coqbot-app coqbot-app Bot removed the needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it. label Jan 15, 2026
proux01
proux01 commented Jan 15, 2026
View reviewed changes
Comment thread algebra/num_theory/orderedzmod.v
Comment on lines +851 to +854
(* TODO: should work for semiring *)
(* Lemma real1 : 1%R \is @real R. Proof. exact: rpred1. Qed. *)
(* Lemma realn n : n%:R \is @real R. Proof. exact: rpred_nat. Qed. *)
(* #[local] Hint Resolve real0 real1 : core. *)

@proux01 proux01 Jan 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe we should open an issue about that to remember to handle it in a future PR?

@proux01

proux01 commented Jan 15, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor Author

Infotheo failure is unrelated, c.f., math-comp/analysis#1822 (comment)

@pi8027 pi8027 self-requested a review January 15, 2026 12:00
proux01
proux01 commented Jan 15, 2026
View reviewed changes
Comment thread algebra/num_theory/orderedzmod.v Outdated
CohenCyril and others added 3 commits January 16, 2026 09:56
@CohenCyril @proux01
Adding numZmodType
06e2a45
@proux01
Generalize lemmas from numDomainType to porderedZmodType
4fd638f 
Only lemmas `addr_gt0`, `mulrn_lgt0`, `pmulrIn` and `lteif_oppE` are
added, everything else is just moved from one section to another.
@CohenCyril @proux01
Generalize lemmas from numDomainType to numZmodType
8d7bef5 
Only lemmas `zmod_leP`, `zmod_ltP`, `zmod_ltgtP`, `zmod_ge0P`,
`zmod_le0P` and `zmod_ltgt0P` are added, everything else is just moved
from one section to another.
@proux01

proux01 commented Jan 16, 2026

Copy link
Copy Markdown
Contributor Author

@CohenCyril CI "green". I can't approve because I'm technically the one who opened the PR but in practice, it is your code that I just extracted from #1338 , split in commits and reviewed. So if you trust my review, you can technically approve your code on my behalf and merge.
I think we shouldn't wait too much to merge this, it is moving quite a bit of code and rebases incur a high risk of accidentally deleting code (I did catch a few instances while doing the changelog).

@CohenCyril CohenCyril merged commit 43f75bb into math-comp:master Jan 16, 2026
141 of 143 checks passed
@proux01 proux01 deleted the numzmodtype branch January 16, 2026 11:45
@proux01 proux01 mentioned this pull request Jan 16, 2026
Merged
4 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@CohenCyril CohenCyril CohenCyril approved these changes

@pi8027 pi8027 Awaiting requested review from pi8027

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

2.6.0

Development

Successfully merging this pull request may close these issues.

2 participants

@proux01 @CohenCyril