search

coq-community / coqeal

The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Other
65 stars 17 forks source link

Consolidation after inclusion of matrix canonical forms #55

Open palmskog opened 2 years ago

palmskog commented 2 years ago

After #54 is merged, we need to consolidate some material and possibly reorganize it a bit. I open this issue as a memento.

So far, we have at least the following mentioned by Cyril:

the companion matrix has been added to mathcomp already.

proux01 commented 2 years ago

We could also clean a bit the ssrcomplement file, once MathComp 1.13 is out and we switch to it.

CohenCyril commented 2 years ago

There should be some refactoring in about similar since the propositional definition is now in mathcomp. CoqEAL provides a decidability result that should establish a correspondence between propositional and boolean versions of similarity.