aboutsummaryrefslogtreecommitdiff
path: root/mathcomp/odd_order
diff options
context:
space:
mode:
authorCyril Cohen2015-07-22 13:11:18 +0200
committerCyril Cohen2015-07-22 13:11:18 +0200
commit80471736932aee0a4287345ea8ffb10ca42b7165 (patch)
treed67abe61bfcbe10f04404c6ee12a2e32e4e30a1c /mathcomp/odd_order
parent6d3dcee3ead208e6e40979ad9252abf192cfbbd7 (diff)
make the opam package meta data
Diffstat (limited to 'mathcomp/odd_order')
-rw-r--r--mathcomp/odd_order/descr6
1 files changed, 6 insertions, 0 deletions
diff --git a/mathcomp/odd_order/descr b/mathcomp/odd_order/descr
new file mode 100644
index 0000000..ee393a9
--- /dev/null
+++ b/mathcomp/odd_order/descr
@@ -0,0 +1,6 @@
+Odd Order Theorem
+
+This library contains the complete formal proof of the Odd Order
+Theorem (aka Feit Thompson Theorem).
+The file stripped_odd_order_theorem.v contains a proof of a self
+contained statement of the odd order. \ No newline at end of file