D. Gorenstein, Finite groups, 1980.

H. Bender and G. Glauberman, Local analysis for the Odd Order Theorem, Number, vol.188, 1994.
DOI : 10.1017/CBO9780511665592

T. Peterfalvi, Character Theory for the Odd Order Theorem. Number 272 in London Mathematical Society Lecture Note Series, 2000.

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, Theorem Proving in Higher-Order Logics, pp.86-101, 2007.
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131

Y. Bertot, G. Gonthier, S. Ould-biha, and I. Pasca, Canonical Big Operators, Theorem Proving in Higher-Order Logics, pp.86-101, 2008.
DOI : 10.1007/3-540-44659-1_29
URL : https://hal.archives-ouvertes.fr/inria-00331193

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Theorem Proving in Higher-Order Logics, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

L. Pottier, User contributions in Coq, Algebra, 1999.

F. Blanqui, S. Coupet-grimal, W. Delobel, and A. Koprowski, Color: a Coq library on rewriting and termination (2006) Eighth Int, Workshop on Termination

P. Rudnicki, C. Schwarzweller, and A. Trybulec, Commutative Algebra in the Mizar System, Journal of Symbolic Computation, vol.32, issue.1-2, pp.143-169, 2001.
DOI : 10.1006/jsco.2001.0456

S. Obua, Proving Bounds for Real Linear Programs in Isabelle/HOL, Theorem Proving in Higher-Order Logics, pp.227-244, 2005.
DOI : 10.1007/11541868_15

J. Harrison, A HOL Theory of Euclidian Space, LNCS, vol.3603, pp.114-129, 2005.

J. Cowles, R. Gamboa, and J. V. Baalen, Using ACL2 Arrays to Formalize Matrix Algebra, 2003.

J. Stein, Documentation for the formalization of Linerar Agebra http

G. Gonthier and A. Mahboubi, A small scale reflection extension for the Coq system
URL : https://hal.archives-ouvertes.fr/inria-00258384

M. Sozeau and N. Oury, First-Class Type Classes, Theorem Proving in Higher Order Logics, 21th International Conference, pp.278-293, 2008.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972