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).
```

That's clearly a bug. Feel free to open an issue or even a PR.

Thanks for pointing that out

Last updated: Jul 15 2024 at 20:02 UTC