Zulip Chat Archive

Stream: new members

Topic: one_mul_eq_id


view this post on Zulip Damiano Testa (Apr 10 2021 at 19:51):

Dear All,

I want to use the first of the four lemmas below: does it already appear in mathlib? If not, should I PR it?

Thanks!

variables  {α : Type*} [monoid α]

@[to_additive]
lemma one_mul_eq_id : has_mul.mul (1 : α) = id := funext $ λ _, (one_mul _).trans (id.def _).symm

@[to_additive]
lemma mul_one_eq_id : (λ x : α, x * 1) = id := funext $ λ _, (mul_one _).trans (id.def _).symm

view this post on Zulip Alex J. Best (Apr 10 2021 at 20:58):

You can also write these like this I believe

import tactic
variables  {α : Type*} [monoid α]

@[to_additive]
lemma one_mul_eq_id : ((*) (1 : α)) = id := funext $ λ _, (one_mul _).trans (id.def _).symm

@[to_additive]
lemma mul_one_eq_id : (* (1 : α)) = id := funext $ λ _, (mul_one _).trans (id.def _).symm

I'm not sure what the preferred way for the library would be, or if there is a genuine difference at all.
Do these versions work in your use-case?

view this post on Zulip Damiano Testa (Apr 10 2021 at 21:03):

The only version that I need (ne_mul_eq_id) works in your form as well!

view this post on Zulip Damiano Testa (Apr 10 2021 at 21:11):

Also, I really only use this lemma once. Maybe it does not make sense to PR it: one of these lemmas is used once, and none of them have been used so far!

view this post on Zulip Yury G. Kudryashov (Apr 10 2021 at 21:54):

Even shorter:

example {M : Type*} [mul_one_class M] : (* (1 : M)) = id := funext mul_one

Last updated: May 13 2021 at 20:13 UTC