Florent Hivert
Florent Hivert
Work on Bruhat order.
Dear Barbichu, I started working with your order.v file and I realized that there are some missing construction. I'm willing to contribute, but I'm really scared by all these Canonical...
In file https://github.com/math-comp/finmap/blob/master/order.v: > latticeType == the type of distributive lattices I.E.: all lattices are assumed to be distributive. There is a lot to say on non-distributive lattices. I'd love...
Consider the following code: ``` Variable (f1 f2 : {fset nat}). Lemma bla : [fset (n1 + n2)%N | n1 in f1, n2 in f2] == fset0. Proof. rewrite /=....
I'm afraid I might be not expert enough with canonical structure to finish my pull request https://github.com/math-comp/finmap/pull/8. Here is what could possibly done 1 - Any subtype of a porder/order...
Note on what we discussed at Dagstuhl 18341: - The name "reverse" order looks bad to me. Indeed the reverse lexicographic order is not the reverse of the lex order....
I have code using Coq/mathcomp which used to work since 8.4 and now breaks with 8.7.0. Depending on the context either it hangs eating all the memory or returns with...
Default constructor for permutation are getting on the way in trivial case. Here is the problem. To construct them we need to: > new Permutation(new std::vector()) > new Permutation(new std::vector({0}))...
##### Add lemmas expressing the inverse of a product This PR add a few missing lemma about products (commutative or not) in unitary ring. The most important one is ```...
Set such as ``` Definition directed (T : Type) (R : T -> T -> bool) := forall x y : T, { z | R x z & R...