# Zulip Chat Archive

## Stream: new members

### Topic: mul_right_comm_monoid

#### Damiano Testa (Apr 09 2021 at 13:08):

I could not find the instances below: am I missing some import? Does it make sense to PR it? Or should the solution be to have only a single `cancel_comm_monoid`

class, instead of `cancel_left_comm_monoid`

,`cancel_right_comm_monoid`

and `cancel_comm_monoid`

, with crossed instances relating them?

```
instance right_of_left {R : Type*} [left_cancel_comm_monoid R] : right_cancel_comm_monoid R :=
{ mul_right_cancel := λ a b c ac, begin
repeat { rw mul_comm _ b at ac},
exact mul_left_cancel ac,
end,
..(infer_instance : left_cancel_comm_monoid R) }
instance left_of_right {R : Type*} [right_cancel_comm_monoid R] : left_cancel_comm_monoid R :=
by apply_instance -- fails
```

#### Damiano Testa (Apr 09 2021 at 13:18):

Here are a bunch of (missing?/unneeded) instances:

```
variable {R : Type*}
instance right_of_left [left_cancel_comm_monoid R] : right_cancel_comm_monoid R :=
{ mul_right_cancel := λ a b c ac, by { repeat { rw mul_comm _ b at ac}, exact mul_left_cancel ac },
..(infer_instance : left_cancel_comm_monoid R) }
instance left_of_right [right_cancel_comm_monoid R] : left_cancel_comm_monoid R :=
{ mul_left_cancel := λ a b c bc, by { repeat { rw mul_comm a at bc}, exact mul_right_cancel bc },
..(infer_instance : right_cancel_comm_monoid R) }
instance cancel_of_left [left_cancel_comm_monoid R] : cancel_comm_monoid R :=
{ ..(infer_instance : left_cancel_comm_monoid R),
..(infer_instance : right_cancel_comm_monoid R) }
instance cancel_of_right [right_cancel_comm_monoid R] : cancel_comm_monoid R :=
{ ..(infer_instance : left_cancel_comm_monoid R),
..(infer_instance : right_cancel_comm_monoid R) }
```

#### Anne Baanen (Apr 09 2021 at 13:21):

docs#left_cancel_comm_monoid, for the lazy like me

#### Damiano Testa (Apr 09 2021 at 13:22):

docs#left_cancel_comm_monoid ← Sorry, simply my attempt at seeing how to generate the link!

#### Damiano Testa (Apr 09 2021 at 13:24):

Unless there is a reason for preferring these typeclasses, I would opt for having a single `cancel_comm_monoid`

typeclass, with "asymmetric" fields, choosing, say, `mul_left_cancel`

.

#### Damiano Testa (Apr 09 2021 at 13:25):

And, if such a thing exist, also `cancel_semigroup`

...

#### Anne Baanen (Apr 09 2021 at 13:25):

Looks like they were added in #3688 and we didn't realize `left`

+ `comm`

is exactly the same as `right`

+ `comm`

.

#### Damiano Testa (Apr 09 2021 at 13:25):

docs#left_cancel_comm_semigroup may not exist...

#### Anne Baanen (Apr 09 2021 at 13:26):

So yes, defining `cancel_comm_monoid extends left_cancel_monoid, comm_monoid`

and then proving `right_cancel`

as well, looks like the best option.

#### Anne Baanen (Apr 09 2021 at 13:26):

(i.e. provide instances `cancel_comm_monoid.to_right_cancel_monoid`

and `cancel_comm_monoid.to_cancel_monoid`

.)

#### Anne Baanen (Apr 09 2021 at 13:27):

Actually, judging from the number of instances, let's promote `right_cancel_comm_monoid`

to be the one true typeclass.

#### Damiano Testa (Apr 09 2021 at 13:27):

...and there are the `add`

versions as well.

#### Anne Baanen (Apr 09 2021 at 13:29):

Unfortunately `@[to_additive]`

can't autogenerate structures (like typeclasses), so we have to write out the class twice :(

#### Damiano Testa (Apr 09 2021 at 13:29):

for the left version, there is this comment in the code:

-- TODO: I found 1 (one) lemma assuming `[add_left_cancel_monoid]`

.

-- Should we port more lemmas to this typeclass?

I guess that I am going to be the one taking, at least in part, this to completion!

#### Damiano Testa (Apr 09 2021 at 13:29):

Anne, or rather, in this case, remove them twice! :upside_down:

#### Damiano Testa (Apr 09 2021 at 13:31):

Ok, so I am going to keep the `right_comm`

code, except that I remove the word `right`

from it. Then, I change the `left_comm`

classes to instance, correct?

#### Damiano Testa (Apr 09 2021 at 13:32):

Finally, I remove what is now `comm`

with no indication of `left/right`

.

From a procedural point of view, I would begin with removing the `comm`

[no left/right], then promote `right_comm`

to `comm`

only and finally instance the `left`

.

#### Anne Baanen (Apr 09 2021 at 13:32):

Sounds good. Don't we have docs#cancel_comm_monoid already?

#### Damiano Testa (Apr 09 2021 at 13:33):

Yes, but it extends both. Ah, I could make it extend only right, erase right and instance left. This is simpler, you are right!

#### Anne Baanen (Apr 09 2021 at 13:33):

So make sure that the "new" `cancel_comm_monoid`

has the same lemmas and instances as the "old" `cancel_comm_monoid`

.

#### Damiano Testa (Apr 09 2021 at 13:34):

I will get down to it! I am sure that lean will let me know if I mess something up...

#### Damiano Testa (Apr 09 2021 at 13:35):

What does `ancestor`

mean below?

```
@[protect_proj, ancestor add_left_cancel_comm_monoid add_right_cancel_comm_monoid]
class add_cancel_comm_monoid (M : Type u)
extends add_left_cancel_comm_monoid M, add_right_cancel_comm_monoid M
```

Should this become

```
@[protect_proj, ancestor add_right_cancel_comm_monoid]
class add_cancel_comm_monoid (M : Type u)
extends add_right_cancel_comm_monoid M
```

#### Anne Baanen (Apr 09 2021 at 13:38):

I am not exactly sure to be honest! I think `protect_proj`

will give the `protected`

attribute to the fields of the structure (so that `cancel_comm_monoid.mul`

doesn't become `mul`

when the `cancel_comm_monoid`

namespace is open).

#### Anne Baanen (Apr 09 2021 at 13:39):

And `ancestor`

is used by the `subtype_instance`

tactic to copy over fields, it looks like. So just copy over what comes after the `extends`

.

#### Anne Baanen (Apr 09 2021 at 13:40):

So `add_cancel_comm_monoid`

would look something like:

```
@[protect_proj, ancestor add_comm_monoid add_right_cancel_monoid]
class add_cancel_comm_monoid (M : Type u)
extends add_comm_monoid M, add_right_cancel_monoid M
```

#### Damiano Testa (Apr 09 2021 at 13:47):

Hence, the `ancestor`

thing will be "forgotten" in the `instance`

from `cancel_comm`

to `cancel_left`

, right?

#### Anne Baanen (Apr 09 2021 at 13:48):

Yes, it is just to keep track of which fields to copy and which ones to add when declaring a new instance via tactics.

#### Eric Wieser (Apr 09 2021 at 13:52):

Why not extend both but fill out the redundant axiom with opt_param?

#### Damiano Testa (Apr 09 2021 at 13:56):

What does opt_param mean?

#### Eric Wieser (Apr 09 2021 at 13:58):

I think src#preorder has an example

#### Eric Wieser (Apr 09 2021 at 13:59):

The `(lt := ...)`

parameter fills that field automatically

#### Damiano Testa (Apr 09 2021 at 13:59):

I had seen this and I remember having been happy that it "just worked". I guess that now is my time to make it "just work", right? :wink:

#### Damiano Testa (Apr 09 2021 at 14:01):

also, when I do this

```
/-- Commutative version of cancel_monoid. -/
@[protect_proj, ancestor right_cancel_monoid left_cancel_monoid comm_monoid, to_additive add_cancel_comm_monoid]
class cancel_comm_monoid (M : Type u) extends
left_cancel_monoid M, right_cancel_monoid M, comm_monoid M
```

`class`

complains:

```
Failed to map fields of cancel_comm_monoid
```

#### Damiano Testa (Apr 09 2021 at 14:02):

This disappears, though, if I remove the line with `@`

#### Damiano Testa (Apr 09 2021 at 14:12):

In fact, simply erasing `to_additive add_cancel_comm_monoid`

is enough to make the error go away.

#### Damiano Testa (Apr 09 2021 at 14:13):

Since the class just above `cancel_comm_monoid`

is `add_cancel_comm_monoid`

, maybe the `to_additive`

is not needed? I would have guessed that `to_additive`

would have created exactly the class that is defined above, right?

#### Damiano Testa (Apr 09 2021 at 14:13):

Ah, Anne said that `to_additive`

does not work with classes...

#### Damiano Testa (Apr 09 2021 at 14:14):

So, I probably need it, but I am not able to make it work.

#### Damiano Testa (Apr 09 2021 at 14:18):

Sorry about the noise: I think that I am making progress! Ignore the previous comments, for the moment!

#### Mario Carneiro (Apr 09 2021 at 14:29):

You need to add the `to_additive`

after the class

#### Damiano Testa (Apr 09 2021 at 14:30):

If the proof of an `instance`

is `by apply_instance`

, then that `instance`

is not needed, correct?

This means that I will want to prove instances `[left_cancel] + [comm] => [cancel] + [comm]`

and similarly for `right`

and then same again for `add`

.

#### Mario Carneiro (Apr 09 2021 at 14:30):

Those don't sound like they should be instances

#### Mario Carneiro (Apr 09 2021 at 14:30):

they will loop

#### Damiano Testa (Apr 09 2021 at 14:31):

Mario, right now, this works:

```
/-- Commutative version of add_cancel_monoid. -/
@[protect_proj, ancestor add_right_cancel_monoid add_left_cancel_monoid add_comm_monoid]
class add_cancel_comm_monoid (M : Type u) extends
add_right_cancel_monoid M, add_left_cancel_monoid M, add_comm_monoid M
/-- Commutative version of cancel_monoid. -/
@[protect_proj, ancestor right_cancel_monoid left_cancel_monoid comm_monoid,
to_additive add_cancel_comm_monoid]
class cancel_comm_monoid (M : Type u) extends
right_cancel_monoid M, left_cancel_monoid M, comm_monoid M
/-- An add_cancel_comm_monoid. -/
instance add_left_cancel_comm_monoid (M : Type u) [add_cancel_comm_monoid M] :
add_left_cancel_monoid M := by apply_instance
```

I imagine that the last instance can be removed. Is the rest looking good?

#### Mario Carneiro (Apr 09 2021 at 14:32):

Don't put `to_additive`

on the class definition

#### Eric Wieser (Apr 09 2021 at 14:32):

Why not on the class definition?

#### Damiano Testa (Apr 09 2021 at 14:32):

Ok, no `instances [left_cancel] + [comm] => [cancel] + [comm]`

. Should there be defs instead? Or simply not there at all?

#### Eric Wieser (Apr 09 2021 at 14:32):

Don't we do that everywhere?

#### Mario Carneiro (Apr 09 2021 at 14:32):

It has to be done after the definition of the class

#### Damiano Testa (Apr 09 2021 at 14:32):

I copied the `to_additive`

adapting what was already there. Still, I am happy to keep it or remove it, as needed-

#### Mario Carneiro (Apr 09 2021 at 14:33):

although maybe my info is out of date, it used to be a lot more annoying

#### Eric Wieser (Apr 09 2021 at 14:33):

Are you sure? I thought that's just because you can't put `to_additive`

on the `mul`

version until the add version is defined

#### Eric Wieser (Apr 09 2021 at 14:33):

And for some reason lots of files define the add version after the mul version

#### Mario Carneiro (Apr 09 2021 at 14:33):

```
/-- A `group` is a `monoid` with an operation `⁻¹` satisfying `a⁻¹ * a = 1`.
There is also a division operation `/` such that `a / b = a * b⁻¹`,
with a default so that `a / b = a * b⁻¹` holds by definition.
-/
@[protect_proj, ancestor div_inv_monoid]
class group (G : Type u) extends div_inv_monoid G :=
(mul_left_inv : ∀ a : G, a⁻¹ * a = 1)
/-- An `add_group` is an `add_monoid` with a unary `-` satisfying `-a + a = 0`.
There is also a binary operation `-` such that `a - b = a + -b`,
with a default so that `a - b = a + -b` holds by definition.
-/
@[protect_proj, ancestor sub_neg_monoid]
class add_group (A : Type u) extends sub_neg_monoid A :=
(add_left_neg : ∀ a : A, -a + a = 0)
attribute [to_additive] group
```

#### Mario Carneiro (Apr 09 2021 at 14:33):

like this

#### Eric Wieser (Apr 09 2021 at 14:34):

Yes, exactly - the attribute is only separate because the definitions are in the wrong order

#### Eric Wieser (Apr 09 2021 at 14:34):

My guess would be that

```
@[foo, bar]
class X
```

and

```
@[foo]
class X
attribute [bar] X
```

are indistinguishable to lean

#### Mario Carneiro (Apr 09 2021 at 14:36):

No, they have different effects, because in the first one `bar`

can act while `X`

is still being constructed, so it can influence the constructors and such

#### Mario Carneiro (Apr 09 2021 at 14:36):

for example `@[class] structure foo := (a : nat)`

vs `structure foo := (a : nat) attribute [class] foo`

have different types for `foo.a`

#### Damiano Testa (Apr 09 2021 at 14:40):

Ok, I feel like the dog playing cards of the memes... the conclusion is that I should put the to additive *after* the definition as an attribute, right?

#### Damiano Testa (Apr 09 2021 at 14:40):

#### Anne Baanen (Apr 09 2021 at 14:42):

I think so: define `class add_cancel_comm_monoid`

, then `class cancel_comm_monoid`

, then `attribute [to_additive] cancel_comm_monoid`

.

#### Damiano Testa (Apr 09 2021 at 14:43):

While I am at it, should the second be the preferred form, then?

```
@[protect_proj, ancestor left_cancel_semigroup monoid, to_additive add_left_cancel_monoid]
class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M
--better as follows than above?
@[protect_proj, ancestor left_cancel_semigroup monoid]
class left_cancel_monoid (M : Type u) extends left_cancel_semigroup M, monoid M
attribute [to_additive] add_left_cancel_monoid
```

#### Damiano Testa (Apr 09 2021 at 15:00):

PR #7134

#### Damiano Testa (Apr 09 2021 at 15:01):

It already has an error. I will try to fix it, but may need further assistance. Sorry for opening this can of worms and not being able to clean up my own mess...

#### Damiano Testa (Apr 09 2021 at 15:11):

Given my very superficial understanding of the discussion above, what is below seem to be in the wrong order: should the two definitions be swapped around?

```
/-- A commutative monoid is a monoid with commutative `(*)`. -/
@[protect_proj, ancestor monoid comm_semigroup]
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
attribute [to_additive] comm_monoid
```

#### Damiano Testa (Apr 09 2021 at 15:12):

(This is the order in which they appear in the file `algebra/group/defs`

.)

#### Eric Wieser (Apr 09 2021 at 15:13):

`attribute [to_additive] add_left_cancel_monoid`

means "`add_left_cancel_monoid`

is the multiplicative version of some additive lemma"

#### Eric Wieser (Apr 09 2021 at 15:13):

Which is obviously not what you meant!

#### Eric Wieser (Apr 09 2021 at 15:13):

That attribute is only supposed to go on multiplicative things

#### Eric Wieser (Apr 09 2021 at 15:14):

I think you probably meant `attribute [to_additive add_left_cancel_monoid] left_cancel_monoid`

#### Damiano Testa (Apr 09 2021 at 15:14):

Ok, but I think that I did not change this: this is what already was in the file *before* I touched it!

(Let me check that this is really true!)

#### Eric Wieser (Apr 09 2021 at 15:14):

(your claim is not really true!)

#### Eric Wieser (Apr 09 2021 at 15:15):

`@[to_additive x] def y`

means "x is the additive version of y"

#### Eric Wieser (Apr 09 2021 at 15:15):

Usually you can omit `x`

and lean works it out from the name

#### Damiano Testa (Apr 09 2021 at 15:17):

Ok, I will change this, but looking at the file in git, I do not think that I wrote this. Still, I am happy to change it! :smile:

#### Damiano Testa (Apr 09 2021 at 15:20):

Is this the correct form, then?

```
/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
/-- A commutative monoid is a monoid with commutative `(*)`. -/
@[protect_proj, ancestor monoid comm_semigroup]
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
attribute [to_additive] add_comm_monoid
```

#### Eric Wieser (Apr 09 2021 at 15:24):

No!

#### Eric Wieser (Apr 09 2021 at 15:25):

You've told lean that `add_comm_monoid`

is the multiplicative version

#### Damiano Testa (Apr 09 2021 at 15:28):

I'm sorry, I am trying to understand and keep everything straight, but I am clearly failing. I will try to produce a better version!

#### Eric Wieser (Apr 09 2021 at 15:29):

That example above isn't copied from group/basic, is assume?

#### Damiano Testa (Apr 09 2021 at 15:29):

This works in this case, right? Or am I still confused?

```
/-- An additive commutative monoid is an additive monoid with commutative `(+)`. -/
@[protect_proj, ancestor add_monoid add_comm_semigroup]
class add_comm_monoid (M : Type u) extends add_monoid M, add_comm_semigroup M
/-- A commutative monoid is a monoid with commutative `(*)`. -/
@[protect_proj, ancestor monoid comm_semigroup]
class comm_monoid (M : Type u) extends monoid M, comm_semigroup M
attribute [to_additive] comm_monoid
```

#### Eric Wieser (Apr 09 2021 at 15:30):

Your last line is different between that snippet and the previous one

#### Eric Wieser (Apr 09 2021 at 15:30):

The most recent one is correct

#### Damiano Testa (Apr 09 2021 at 15:30):

The very first one was, the one with the comm_monoid *before* the `add_comm_monoid*.

#### Damiano Testa (Apr 09 2021 at 15:30):

Yes, I changed the last line, since I imagine that that would fix the issue...

#### Eric Wieser (Apr 09 2021 at 15:31):

That most recent one looks fine, and it doesn't care what order the two classes go in as long as the attribute is after both

#### Damiano Testa (Apr 09 2021 at 15:32):

Finally I did something right!

#### Damiano Testa (Apr 09 2021 at 15:33):

So, as a "generic rule", the name not inside the square brackets should *not* had `add`

, correct?

#### Damiano Testa (Apr 09 2021 at 15:35):

To be honest, I had completely missed the distinction between inside and outside the square brackets. I hope that I have it straight now.

#### Kevin Buzzard (Apr 09 2021 at 15:44):

`@[to_additive x] def y`

attaches the attribute to `y`

. `attribute [to_additive] x`

attaches the attribute to `x`

.

#### Kevin Buzzard (Apr 09 2021 at 15:45):

You either attach the tag when you're making the definition (e.g. `@[simp] theorem blah...`

) or you attach the tag afterwards (e.g. `theorem blah...`

and then later `attribute [simp] blah`

).

#### Damiano Testa (Apr 09 2021 at 15:46):

Ah, Kevin, one more "subtlety" that I had missed! Anyway, the PR has been building for over 5s now, so it must all be correct... :upside_down:

#### Kevin Buzzard (Apr 09 2021 at 15:47):

You can use `#print blah`

to see all the tags attached to the definition/theorem called `blah`

-- they appear at the very top of the output.

#### Damiano Testa (Apr 09 2021 at 15:48):

Also, from the discussion above, I gathered that `@[to_additive]`

and `attribute [to_additive]`

are not equivalent and the latter seems to be preferred.

#### Kevin Buzzard (Apr 09 2021 at 15:49):

I think they are equivalent. I think you're confused because the `to_additive`

attribute can take other inputs.

#### Kevin Buzzard (Apr 09 2021 at 15:50):

here is an example in mathlib where the to_additive attribute is actually taking an input -- a string, which is the docstring for the additive version. `to_additive`

is a very flexible attribute and I completely agree that there is right now no good place to read about how it works.

#### Damiano Testa (Apr 09 2021 at 15:50):

Kevin, this is what made me say what I did: honestly, I do not understand what the difference is/might be/isn't!

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/mul_right_comm_monoid/near/233831681

#### Kevin Buzzard (Apr 09 2021 at 15:51):

The things you wrote above are equivalent, because you didn't give `to_additive`

any inputs. The fun starts when you add other attributes at the same time, or add attributes which do funky stuff.

#### Damiano Testa (Apr 09 2021 at 15:53):

I am confused on so many levels that I do not even make sense to myself...

#### Kevin Buzzard (Apr 09 2021 at 15:54):

For example `@[simp, to_additive] def x...`

is different to `@[to_additive, simp] def x...`

because in the first one the additivised version of x will also get the simp attribute.

#### Kevin Buzzard (Apr 09 2021 at 15:57):

some attributes are quite powerful and subtle things, and `to_additive`

is one of them. The way I learnt how it worked was just by looking at files like submonoid.basic and making sure I understood what was going on and why things were done the way they were done. But I guess what really taught me was writing some code like this myself, and being forced to learn it (like you are now).

#### Kevin Buzzard (Apr 09 2021 at 15:59):

I think that when I was at your stage (a competent Lean programmer and a mathematician) I started to ask myself whether I could actually *completely* understand random Lean files in mathlib, as opposed to just "basically understanding what was going on". I still ignore pretty much all `meta`

and `do`

code, but everything else I decided that I should probably be able to get to the bottom of it (and of course there are mathematicians who decide to understand `meta`

code too...)

#### Damiano Testa (Apr 09 2021 at 16:00):

Ok, thanks for the encouragement! I think that the PR is building now, so I must have learned *something*! :upside_down:

#### Bryan Gin-ge Chen (Apr 09 2021 at 16:01):

Custom attributes like `to_additive`

and `simps`

(but not `simp`

, I think) are basically metaprograms like tactics that run as Lean processes a declaration. We should expand the documentation if the way to use one isn't completely clear.

#### Kevin Buzzard (Apr 09 2021 at 16:03):

You should write some `to_additive`

doc before you forget everything. The basic things are: (1) basic usage (it makes an additive version of a multiplicative lemma) (2) add the attribute after `simp`

if you want the `simp`

to apply to the additive version (3) for structures (rather than theorems) you have to make the structure yourself and then tag it later (your confusion about adding the attribute at the same time or afterwards) (4) link to the "dictionary" which auto-generates things like theorem names (5) how to override docstrings e.g. with `add_decl_doc`

(see for example line 279 of submonoid.basic, I linked to the file above) (6) the gotcha with g^n vs n smul g and how it breaks everything.

#### Damiano Testa (Apr 09 2021 at 16:03):

Well, at the moment, I am having difficulty even keeping track of whether something is inside or outside some brackets, so my issues are probably at a more fundamental level than what the documentation might say.

That and having to keep track of whether there was an `add`

or not, a `right + comm`

or not really crossed my eyes!

#### Damiano Testa (Apr 09 2021 at 16:04):

Ok, I might give this a shot! Actually, your summary is already clearer than what is in my mind...

#### Kevin Buzzard (Apr 09 2021 at 16:07):

oh also the docstring trick

```
/-- multiplicative docstring -/
@[to_additive "additive docstring"] def gi : galois_insertion...
```

and the "choose another name rather than the auto-generated one" trick e.g.

```
@[to_additive ordered_add_comm_group.add_lt_add_left]
lemma ordered_comm_group.mul_lt_mul_left' (a b : α) (h : a < b) (c : α) : c * a < c * b :=
```

(remove the prime, because there will be some ring version which doesn't have an additive counterpart)

#### Yakov Pechersky (Apr 09 2021 at 16:09):

The final aspect is tagging something with `to_additive`

"out of band", that is, via an `attribute ...`

line like at

```
@[simp] lemma order_of_one : order_of (1 : α) = 1 :=
begin
apply le_antisymm,
{ exact order_of_le_of_pow_eq_one (nat.one_pos) (pow_one 1) },
{ exact nat.succ_le_of_lt ( order_of_pos' ⟨1, ⟨nat.one_pos, pow_one 1⟩⟩) }
end
@[simp] lemma add_order_of_zero : add_order_of (0 : H) = 1 :=
by simp [← order_of_of_add_eq_add_order_of]
attribute [to_additive add_order_of_zero] order_of_one
```

#### Damiano Testa (Apr 09 2021 at 16:41):

Is there a way to get Lean to list the attributes of a given lemma? Say that I want to discover whether an autogenerated lemma is or isn't `simp`

: chan I `#check`

or `#print`

or something like this to find out?

#### Kevin Buzzard (Apr 09 2021 at 16:49):

`#print`

and look at the very top of the output.

#### Damiano Testa (Apr 09 2021 at 16:57):

Thanks, Kevin!

#### Damiano Testa (Apr 09 2021 at 19:47):

To my surprise, once I fixed the silly errors that I introduced, PR #7134 "just worked"! The 4 typeclasses `(add_)left_cancel_comm_monoid, (add_)right_cancel_comm_monoid`

can leave mathlib and no one would notice...

#### Damiano Testa (Apr 09 2021 at 20:22):

I also just noticed that this might be the first time that a PR of mine actually has a net *negative* effect on the number of lines of code in mathlib.

#### Anne Baanen (Apr 09 2021 at 21:19):

Damiano Testa said:

I also just noticed that this might be the first time that a PR of mine actually has a net

negativeeffect on the number of lines of code in mathlib.

"Fools ignore complexity. Pragmatists suffer it. Some can avoid it. Geniuses remove it." Congratulations, you are now a genius :)

#### Notification Bot (Apr 10 2021 at 00:05):

This topic was moved by Scott Morrison to #Is there code for X? > mul_right_comm_monoid

Last updated: May 11 2021 at 23:11 UTC