lemma name

Stream: general

[Yury G. Kudryashov]

How should I call these lemmas?

lemma units.TODO_name {M : Type*} [monoid M] {α : Type*} [mul_action M α]
  (u : units M) (x : α) :
  (↑u⁻¹:M) • (u:M) • x = x :=
by rw [smul_smul, u.inv_mul, one_smul]

lemma units.TODO_name2 {M : Type*} [monoid M] {α : Type*} [mul_action M α]
  (u : units M) (x : α) :
  (u:M) • (↑u⁻¹:M) • x = x :=
by rw [smul_smul, u.mul_inv, one_smul]

[Yury G. Kudryashov]

I found myself doing this rw from right to left more than once, so I assume that it should be a named lemma.

[Johan Commelin]

inv_smul_self_smul?

[Reid Barton]

smul_inv_smul?

[Yury G. Kudryashov]

Sorry, forgot to add the other one.

[Yury G. Kudryashov]

inv_smul_self_smul and self_smul_inv_smul?
smul_inv_smul and smul_smul_inv?

[Reid Barton]

smul_smul_inv for the second

[Reid Barton]

I guess you could put smul and inv in either order, I don't think we're very consistent about this

[Reid Barton]

By the way, do you really need both the up arrow and the :M?

[Yury G. Kudryashov]

Up arrow tells it to coerce after ⁻¹

[Yury G. Kudryashov]

(deleted)

[Johan Commelin]

The dutch verb "smullen" means "to enjoy/feast some food" as in "yummy yummy".
So smul_smul_* reads quite funny to me.

[Johan Commelin]

I suggest yummy_yummy_inv