## Stream: general

### Topic: lemma name

#### Yury G. Kudryashov (May 15 2020 at 20:11):

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 (May 15 2020 at 20:12):

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 (May 15 2020 at 20:12):

inv_smul_self_smul?

#### Reid Barton (May 15 2020 at 20:12):

smul_inv_smul?

#### Yury G. Kudryashov (May 15 2020 at 20:13):

Sorry, forgot to add the other one.

#### Yury G. Kudryashov (May 15 2020 at 20:14):

inv_smul_self_smul and self_smul_inv_smul?
smul_inv_smul and smul_smul_inv?

#### Reid Barton (May 15 2020 at 20:14):

smul_smul_inv for the second

#### Reid Barton (May 15 2020 at 20:14):

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

#### Reid Barton (May 15 2020 at 20:15):

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

#### Yury G. Kudryashov (May 15 2020 at 20:15):

Up arrow tells it to coerce after ⁻¹

(deleted)

#### Johan Commelin (May 15 2020 at 20:17):

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

#### Johan Commelin (May 15 2020 at 20:17):

I suggest yummy_yummy_inv

Last updated: May 14 2021 at 21:11 UTC