IsROrC.ofReal = Complex.ofReal'

Stream: Is there code for X?

[Ruben Van de Velde]

Do we have any lemma to rewrite IsROrC.ofReal when applies to \C?

[Jireh Loreaux]

I think not, although I'm curious where it came up that you need it.

[Jireh Loreaux]

Putting it immediately after docs#Complex.instIsROrCComplex makes sense.

[Yaël Dillies]

I discussed this with @Eric Wieser and I argued that we should not even have to state this since all coercions between two types should syntactically be the same.

[Yaël Dillies]

Understand: Don't write the lemma! Fix mathlib so that the coercions are not even different in the first place.

[Eric Rodriguez]

Don't write the lemma! Spend hours and hours fixing stuff instead and encourage ugly workarounds because few people actually have the time!

[Eric Wieser]

In lean 3 the coercions were already the same

[Jireh Loreaux]

@Yaël Dillies, they're defeq, but in this case it's impossible for them to be exactly the same.

[Jireh Loreaux]

(unless you bring back coe)

[Yaël Dillies]

Why? You can just not define Complex.ofReal' and do everything in terms of IsROrC.ofReal.

[Ruben Van de Velde]

Hmm, does that work for the reals as well?

[Eric Wieser]

Or we eliminate both and use algebraMap everywhere

[Yaël Dillies]

Ruben Van de Velde said:

Hmm, does that work for the reals as well?

Technically, yes. It's the identity coercion. I wonder how it's not causing problems, actually. :thinking: