lemmas for add_equiv

Stream: new members

[Andre Knispel]

There are many lemmas for mul_equiv that don't seem to exist for add_equiv. Is there some way of converting them, or can I use them somehow without duplicating them?

[Kevin Buzzard]

Can you give an example?

[Andre Knispel]

There is map_one, saying that mul_equiv respects 1, but I can't find the equivalent one in the additive case

[Kevin Buzzard]

import tactic

#check mul_equiv.map_one
#check add_equiv.map_zero

Both work fine for me.

[Kevin Buzzard]

@[simp, to_additive]
lemma map_one {M N} [monoid M] [monoid N] (h : M ≃* N) : h 1 = 1 :=
by rw [←mul_one (h 1), ←h.apply_symm_apply 1, ←h.map_mul, one_mul]

That to_additive attribute that the lemma is tagged with, means "automatically generate the additive version and give it an appropriate name"; you won't see the proof of the additive version explicitly in mathlib because it's auto-generated by the system.

[Andre Knispel]

Ah, I see, thanks! I didn't expect that!

[Kevin Buzzard]

Attributes are some of the hardest things to figure out in Lean. They are not particuarly well documented. When you type @[foo] lemma bar ... then all this means that Lean tags bar with the foo attribute. Some of these attributes are little more than labels, e.g. tagging something with simp just says "simplifier, use me if you need me", but other tags actually make stuff happen on the spot. We should have a list somewhere. Is there a list somewhere? I've just picked them up from seeing them so many times.

[Andre Knispel]

Are they builtins? Or is there e.g. some fancy metaprogram that generates the additive version if it sees such a tag?

[Reid Barton]

There are both kinds, but to_additive is implemented in mathlib: src#to_additive.attr

[Yury G. Kudryashov]

More precisely: @[foo] lemma bar means that once lemma bar is parsed and added to the environment, Lean will run the function associated with attribute foo. This function can do whatever it wants. to_additive parses both declaration and definition of its argument and tries to generate the corresponding lemma/def with all * replaced with + etc.

[Bryan Gin-ge Chen]

There is a doc page on to_additive now (suggestions welcome!): https://leanprover-community.github.io/mathlib_docs/attributes.html#to_additive