Stream: math-comp users

Topic: Matrix canonical forms repo


view this post on Zulip Karl Palmskog (Sep 07 2021 at 16:34):

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

view this post on Zulip Karl Palmskog (Sep 07 2021 at 16:37):

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

view this post on Zulip Pierre Roux (Sep 07 2021 at 17:44):

If it builds on CoqEAL, that could indeed make sense.

view this post on Zulip Karl Palmskog (Sep 07 2021 at 18:05):

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