Open
Description
In previous version(1.1.4) of mathcomp/real-closed, by the definition of Rcomplex, the users can choose R[i] to be canonical to lmodType R or lmodType R[i].
Definition Rcomplex := complex.
Canonical Rcomplex_eqType (R : eqType) := [eqType of Rcomplex R].
Canonical Rcomplex_countType (R : countType) := [countType of Rcomplex R].
Canonical Rcomplex_choiceType (R : choiceType) := [choiceType of Rcomplex R].
Canonical Rcomplex_zmodType (R : rcfType) := [zmodType of Rcomplex R].
Canonical Rcomplex_ringType (R : rcfType) := [ringType of Rcomplex R].
Canonical Rcomplex_comRingType (R : rcfType) := [comRingType of Rcomplex R].
Canonical Rcomplex_unitRingType (R : rcfType) := [unitRingType of Rcomplex R].
Canonical Rcomplex_comUnitRingType (R : rcfType) := [comUnitRingType of Rcomplex R].
Canonical Rcomplex_idomainType (R : rcfType) := [idomainType of Rcomplex R].
Canonical Rcomplex_fieldType (R : rcfType) := [fieldType of Rcomplex R].
Canonical Rcomplex_lmodType (R : rcfType) :=
LmodType R (Rcomplex R) (ComplexField.complex_lmodMixin R).
However, in the latest version 2.0.0, the sixth line complex_lmodMixin did not use Rcomplex, resulting in R[i] be canonical to lmodType R by default, and I don't know how to avoid this. In fact, R[i] should be canonical to lmodType R[i] in many cases. For example, R[i] should be normedModType C when considering its topological structure.
Definition Rcomplex := complex.
HB.instance Definition _ (R : eqType) := Equality.on (Rcomplex R).
HB.instance Definition _ (R : countType) := Countable.on (Rcomplex R).
HB.instance Definition _ (R : choiceType) := Choice.on (Rcomplex R).
HB.instance Definition _ (R : rcfType) := GRing.Field.on (Rcomplex R).
HB.instance Definition _ (R : rcfType) := complex_lmodMixin R.
HB.instance Definition _ (R : rcfType) := complex_lalgMixin R.
HB.instance Definition _ (R : rcfType) := GRing.Lalgebra.on (Rcomplex R).
Metadata
Metadata
Assignees
Labels
No labels