search

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

Prove that polynomials form a ring #42

Closed johanneskloos closed 7 years ago

johanneskloos commented 7 years ago

Prove that the definition of polynomials via lists satisfies all the ring axioms. Some existing proofs were changed a bit, mostly to simplify them or make use of lemmas that were introduced in the course of proving other properties.

spitters commented 7 years ago

Thanks!