Naming of lemmas about / and % on Int

Stream: mathlib4

[Michael Stoll]

While trying to find a home for

theorem Int.mul_ediv_le {m : ℤ} (h : 0 < m) (n : ℤ) : m * (n / m) ≤ n := ...

I noticed that relevant lemmas in Std.Data.Int.DivMod use ediv and emod in their names (e.g., docs#Int.ediv_add_emod, which is used in the proof), whereas in Mathlib, we have, e.g., docs#Int.eq_of_mod_eq_of_natAbs_sub_lt_natAbs (in Mathlib.Data.Int.Div).

What is the naming convention here? Should the lemma above be Int.mul_div_le instead?

[Michael Stoll]

:ping_pong: It would be nice to get some reaction to this question. Is there a convention? Are there opionions?

[Yaël Dillies]

Use div and mod. ediv and emod are only used in Core and Std lemma names.

[Yaël Dillies]

mathlib overrides the definition of div and mod to be ediv and emod instead of quot and rem.

[Michael Stoll]

OK, thanks!
It is a bit unfortunate that there is some inconsistency here between Core/Std and Mathlib, but I guess it can't really be helped.

[Yaël Dillies]

We're not changing the mathlib definition because this is the mathematically sensible one. So the only way out is if core Lean changed its mind, which it probably won't either.

[Scott Morrison]

From memory long ago core agreed to change, but it is not high priority to actually do so. I think everyone agrees the Mathlib conventions are the correct optimal ones.