Stream: math-comp users

Topic: Question on ssralg


view this post on Zulip Zhangsheng Lai (Apr 14 2021 at 16:17):

Hi, I'm reading the ssralg algebraic hierarchy trying to understand the structure defined in it. In it there are some definitions prefixed by GRing found here. Could someone explain what do those mean and also if anyone knows if there are other materials with a more gentle introduction of the ssralg.v library ?

view this post on Zulip Enrico Tassi (Apr 14 2021 at 16:22):

GRing is just a namespace, you will also find FinRing and CountRing.
I would not spend too much time understanding the details of ssralg, since it is undergoing a massive simplification here: https://github.com/math-comp/math-comp/pull/733
The new code should be more readable, look for HB.structure to find all structures defined in the file.


Last updated: Feb 08 2023 at 08:02 UTC