X is a regular element in the ring of list-based polynomials - Githubissues

agda / cubical

An experimental library for Cubical Agda

https://agda.github.io/cubical/Cubical.README.html

Other

454 stars 139 forks source link

X is a regular element in the ring of list-based polynomials #919

Closed felixwellen closed 2 years ago

felixwellen commented 2 years ago

This means that multiplication with X is injective. Depends on #917