RCLike.zero_re'

Stream: mathlib4

[Iván Renison]

Hi, in Mathlib.Analysis.RCLike.Basic we have this lemma:

@[rclike_simps]
theorem zero_re' : re (0 : K) = (0 : ℝ) :=
  map_zero re

I want to ask:
1) Why is zero_re' instead of zero_re?
2) Do we have version for im?

[Aaron Liu]

It looks like zero_re' was added in mathlib3#4057 and zero_re was deleted in mathlib3#4824

[Jireh Loreaux]

This is misnamed anyway, it should be re_zero

[Jireh Loreaux]

docs#RCLike.zero_re

[Jireh Loreaux]

docs#RCLike.re_zero

[Yury G. Kudryashov]

Many lemmas about RCLike use re and im as suffixes, probably after Complex lemmas.

[Yury G. Kudryashov]

Do you remember what was the outcome of the recent discussion about that?

[Yury G. Kudryashov]

(I mean, whether we should continue using projections as suffixes here and there, or switch to prefixes).

[Iván Renison]

I opened #25077 removing de ' of zero_re and adding zero_im

[Yaël Dillies]

Yury G. Kudryashov said:

Many lemmas about RCLike use re and im as suffixes, probably after Complex lemmas.

I did rename a lot of those lemmas back then. Let's not add any more please

[Eric Wieser]

As is, let's use prefices?