Skip to content

An attempt to recreate a simple proof that all functions between fields can be decomposed into the sum of an even and an odd function.

License

Notifications You must be signed in to change notification settings

nbrader/proofs-odd-and-even-parts

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

26 Commits
 
 
 
 
 
 
 
 
 
 

Repository files navigation

An attempt to recreate a simple proof that all functions between fields can be decomposed into the sum of an even and an odd function.

In order to view these files with the intended Coq parser, you should install:

  • Visual Studio Code (1.94.2)
  • VsCoq (v2.1.2)

You may find that Coq .v files can only be found by other Coq .v files when you've opened in Visual Studio Code the folder that directly contains that file (and not the parent folder) of multiple folders of .v files.

To build the project, locate the file called build_coq.sh and run it from the command line by typing "ctrl+'" and entering: ./build_coq.sh

Sometimes, the line endings aren't readable and you will first need to run: dos2unix build_coq.sh

About

An attempt to recreate a simple proof that all functions between fields can be decomposed into the sum of an even and an odd function.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published