Nat.mul_eq and Nat.mul_def

Stream: mathlib4

[Alex Meiburg]

Both Nat.mul_eq and Nat.mul_def seem to exist, and they have exactly the same type signature. Is there a reason (besides 'history')?

[Yury G. Kudryashov]

I guess, the only reason is history. docs#Nat.mul_eq is in Lean source code while docs#Nat.mul_def is in Mathlib, migrated from mathlib3.

[Yury G. Kudryashov]

Feel free to submit a PR that turns Nat.mul_def into a deprecated alias for Nat.mul_eq.

[Kim Morrison]

Hmm, maybe careful here. Note that Std adds lemmas like Int.add_def and Int.mul_def, so it's not like there's a consistency before Mathlib arrives!

[Yury G. Kudryashov]

So, what should we do?

[Yaël Dillies]

Rename the core one to Nat.mul_def?

[Eric Wieser]

Or at least upstream Nat.mul_def to Std, since the consistency is with other names there