one_mul_eq_id

Stream: new members

[Damiano Testa]

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

[Alex J. Best]

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?

[Damiano Testa]

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

[Damiano Testa]

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]

Even shorter:

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