lemma 7 #9
Annotations
10 warnings
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.addNr by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.opp by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.add0r by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.addrC by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.addrA by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.add by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L171
Ignoring canonical projection to GRing.isZmodule.zero by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L382
Ignoring canonical projection to GRing.isZmodule.addNr by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L382
Ignoring canonical projection to GRing.isZmodule.opp by
|
build (mathcomp/mathcomp:2.0.0-coq-8.18):
allumette.v#L382
Ignoring canonical projection to GRing.isZmodule.add0r by
|