## Stream: new members

### Topic: one_mul_eq_id

#### 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 α]

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


#### Alex J. Best (Apr 10 2021 at 20:58):

You can also write these like this I believe

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

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?

#### Damiano Testa (Apr 10 2021 at 21:03):

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

#### 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!

#### 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