IsROrC vs Complex

Stream: mathlib4

[Yaël Dillies]

In case people haven't noticed, the coercion ℝ → ℂ is not syntactically the same as the coercion ℝ → 𝕜 where IsROrC 𝕜 and 𝕜 is ℂ. This means that lemma pairs like docs#Complex.ofReal_sum and docs#IsROrC.ofReal_sum are not interchangeable anymore.

[Yaël Dillies]

I find that mildly worrying. What about you?

[Eric Wieser]

(the extra context here is that the lean 3 coe mechanism meant these were syntactically the same)

[Eric Wieser]

I don't think this is any more worrying than having two different .ims

[Yaël Dillies]

Really? I had both coercions in the infoview and nothing told they were different until I clicked on them!

[Yaël Dillies]

It's pretty easy to fix as well: Just don't define the coercion ℝ→ ℂ, or define it in terms of the IsROrC one.

[Eric Wieser]

The same solution could work for .re and .im

[Yaël Dillies]

But IsROrC.im is visually different to Complex.im. I don't get your argument...

[Yaël Dillies]

Also the same couldn't really work for .re and .im since you'd lose dot notation.

[Yaël Dillies]

For context, I just lost 40min debugging a rw call that broke because of that.

[Jireh Loreaux]

Sorry, you mean the coercion the other way right? There is no coercion ℂ → ℝ.

[Eric Wieser]

Using algebraMap everywhere would solve this I think

[Eric Wieser]

I think we started doing that in lean 3, but it got in the way of the port so we reverted it all

[Yaël Dillies]

Jireh Loreaux said:

Sorry, you mean the coercion the other way right? There is no coercion ℂ → ℝ.

Uh yeah, of course. Can you tell I'm tired? :grinning: