1 search result for "tag:"logpath:mathcomp.contrib.sum_of_two_square""

A proof of Fermat's theorem on sum of two squares. It is the proof that uses gaussian integers. This is done in ssreflect. It contains two file :