Formalising Sylow's theorems in Coq

Details Formalising Sylow's theorems in Coq Formalising Sylow's theorems in Coq

2006-11-14

arxiv.org/abs/cs/0611057v1

Computer Science

Logic in Computer Science

Scientific paper

This report presents a formalisation of Sylow's theorems done in {\sc Coq}. The formalisation has been done in a couple of weeks on top of Georges Gonthier's {\sc ssreflect} \cite{ssreflect}. There were two ideas behind formalising Sylow's theorems. The first one was to get familiar with Georges way of doing proofs. The second one was to contribute to the collective effort to formalise a large subset of group theory in {\sc Coq} with some non-trivial proofs.}

Affiliated with

Also associated with

No associations

Rating

Formalising Sylow's theorems in Coq does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.

If you have personal experience with Formalising Sylow's theorems in Coq, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Formalising Sylow's theorems in Coq will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-487863