Zulip Chat Archive

Stream: general

Topic: lemma name


view this post on Zulip 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]

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 15 2020 at 20:12):

inv_smul_self_smul?

view this post on Zulip Reid Barton (May 15 2020 at 20:12):

smul_inv_smul?

view this post on Zulip Yury G. Kudryashov (May 15 2020 at 20:13):

Sorry, forgot to add the other one.

view this post on Zulip 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?

view this post on Zulip Reid Barton (May 15 2020 at 20:14):

smul_smul_inv for the second

view this post on Zulip 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

view this post on Zulip Reid Barton (May 15 2020 at 20:15):

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

view this post on Zulip Yury G. Kudryashov (May 15 2020 at 20:15):

Up arrow tells it to coerce after ⁻¹

view this post on Zulip Yury G. Kudryashov (May 15 2020 at 20:16):

(deleted)

view this post on Zulip 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.

view this post on Zulip Johan Commelin (May 15 2020 at 20:17):

I suggest yummy_yummy_inv


Last updated: May 14 2021 at 21:11 UTC