Skip to content

Commit 3d372c8

Browse files
proux01proux01
committed
Add Pol to mpoly refinement
Apparently commutativity of C is not needed for addition and subtraction, it only became needed for PmulC_aux. Requires math-comp/math-comp#1448 and math-comp#106
1 parent 4011bab commit 3d372c8

File tree

2 files changed

+1049
-0
lines changed

2 files changed

+1049
-0
lines changed

‎_CoqProject‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ src/monalg.v
33
src/mpoly.v
44
src/ssrcomplements.v
55
src/xfinmap.v
6+
src/Pol_mpoly.v
67

78
-R src mathcomp.multinomials
89
-arg -w -arg -ambiguous-paths

0 commit comments

Comments
 (0)