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

Showing 1 - 1
  1. coq-mathcomp-sum-of-two-square

    No documentation

    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 :
    logpath:mathcomp.contrib.sum_of_two_square
    Laurent Thery
    1.0.1
    MIT
    Used by 0 other packages
    09 May 2018