Stream: math-comp users

Topic: Missing join of NormedZmodule and POrderZmodule


view this post on Zulip Li Zhou (Feb 26 2024 at 18:12):

In mathcomp/algebra/ssrnum.v, there is no join of NormedZmodule and POrderZmodule. The structure inherits from both is numDomainType, which adds isNumRing properties.
This makes defining any types that inherits from NormedZmodule and POrder but lacking isNumRing impossible. For example:

#[short(type="porderNormedLModType")]
HB.structure Definition porderNormedLModule (R : numDomainType) := { T of
    GRing.Lmodule R T &
    Num.POrderedZmodule T &
    Num.NormedZmodule R T
  }.

fails with message
`Error: You must declare the hierarchy bottom-up or addd a missing join. There are two ways out:

Both suggestions fail unless some changes are made to ssrnum.v before declaring numDomainType.
More specifically, we formalized some theories of ordered topological vector space (inherits from both Porder and normedZmodule, but not a numDomainType), and we faced this problem when we updated from mathcomp.1.9.0 to 2.2.0.

Any suggestions to solve the problem? In particular, is there a third suggestion that doesn't need to modify mathcomp?


Last updated: Jul 23 2024 at 20:01 UTC