Thanks to porting work by Yves Bertot, the development by Guillaume Cano from 2014 on normal forms for matrices (building towards Perron-Frobenius) is now compatible with MC 1.12.0 and beyond and has found a home in coq-community: https://github.com/coq-community/matrix_canonical_forms
since this a relatively small repo (~2500 LOC), it may be worth considering incorporating this code into a larger MC-based repo, e.g., CoqEAL
If it builds on CoqEAL, that could indeed make sense.
yeah, it's highly dependent on CoqEAL. The main "cost" to CoqEAL would be introducing a dependency on mathcomp-real-closed
Last updated: Feb 08 2023 at 04:04 UTC