Skip to content

Pull requests: math-comp/math-comp

New pull request New
41 Open 1,088 Closed
41 Open 1,088 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Reviews
Filter by reviews
No reviews Review required Approved review Changes requested
Assignee
Filter by who’s assigned
Assigned to nobody Loading
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Pull requests list

Add numZmodType
#1520 opened Jan 13, 2026 by proux01 • Draft
3 of 4 tasks
Lock form_of_matrix
#1519 opened Jan 13, 2026 by proux01 Loading…
2 of 4 tasks
Better document %num in ssrnat.v
#1518 opened Jan 13, 2026 by proux01 Loading… 2.6.0
1
lemmas from MathComp-Analysis' unstable.v kind: enhancement Issue or PR about addition of features.
#1515 opened Jan 1, 2026 by affeldt-aist Loading…
3 of 4 tasks
2.6.0
6
Added lemma uniq_map_indexE and uniq_map_in_inj to seq kind: enhancement Issue or PR about addition of features.
#1514 opened Dec 28, 2025 by hivert Loading…
2 of 4 tasks
3
define joins of POrderedZmodule and (Semi)NormedZmodule
#1513 opened Dec 26, 2025 by zhou31416 Loading…
4 tasks
7
HB.pack -> HB.enrich
#1511 opened Dec 21, 2025 by gares • Draft
1
More Archimedan lemmas
#1510 opened Dec 4, 2025 by pi8027 • Draft
4 tasks
1
4
rename GRing.exp to pown kind: refactoring Issue or PR about a refactoring. (reorganizing the code, reusing theorems, simplifications...)
#1503 opened Nov 27, 2025 by affeldt-aist Loading…
4 tasks done
2.6.0
24
Introduce proper (semi)vector space structures to fix the ring and algebra instances on 'End(vT)
#1492 opened Nov 5, 2025 by pi8027 Loading…
4 tasks done
2.6.0
1
2
wip: adding interval inference for natural numbers
#1485 opened Oct 13, 2025 by hoheinzollern • Draft
4 tasks
2
lra/nra/psatz/ring/field without Stdlib
#1456 opened Aug 27, 2025 by proux01 Loading…
16 tasks done
2.6.0
11
Tensor formalization
#1446 opened Jul 24, 2025 by joshua-smart • Draft
4 tasks
8
Implemented wrapping of mixin in bigop.v for files monoid.v and nmodule.v
#1435 opened May 19, 2025 by CalosciMatteo • Draft
4 tasks
Remove the workarounds introduced in #1125 drops: coq 8.20 kind: clean-up This issure/PR is about cleaning up obsolete code, removing hacks, etc
#1365 opened Mar 19, 2025 by pi8027 • Draft
4 tasks
2.6.0
40
[Draft] Adding ordered zmodules and extended real numbers
#1338 opened Feb 5, 2025 by CohenCyril • Draft
6 tasks
11
Characteristic for all
#1308 opened Nov 29, 2024 by Tragicus • Draft
4 tasks done
Complements to math-comp originating from the trajectories proofs
#1299 opened Nov 27, 2024 by ybertot • Draft
1 of 4 tasks
2.6.0
1
Fix the notation scope of function notations in ssralg (#978)
#1213 opened Apr 23, 2024 by pi8027 • Draft
2 of 4 tasks
2.6.0
1
8
falgebra and fieldext parts of CohenCyril's abel backports needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment.
#1202 opened Apr 2, 2024 by Tragicus Loading…
3 of 4 tasks
2.6.0
3
Remove the phantom in tuple
#1200 opened Mar 29, 2024 by CohenCyril • Draft
4 tasks
2.6.0
7
finmap needs: rebase PR which is not rebased: check the target is appropriate (generally master) and rebase on top of it.
#1138 opened Dec 11, 2023 by gares • Draft 100+
4
Inductive principles on set cardinality
#1120 opened Nov 6, 2023 by pPomCo Loading…
3 of 4 tasks
2.6.0
5
Contrib bigop
#1119 opened Nov 6, 2023 by pPomCo Loading…
2 of 4 tasks
2.6.0
@Tragicus
19
Contrib finset
#1118 opened Nov 6, 2023 by pPomCo Loading…
2 of 4 tasks
2.6.0
@CohenCyril
5
ProTip! Find all pull requests that aren't related to any open issues with -linked:issue.