llee454 / functional-algebra Goto Github PK
View Code? Open in Web Editor NEWThis package provides a Coq formalization of abstract algebra using a functional programming style. The modules contained within the package span monoids, groups, rings, and fields and provides both axiom definitions for these structures and proofs of foundational results. The current package contains over 800 definitions and proofs.
License: GNU Lesser General Public License v3.0