to_additive

Stream: new members

[Paul van Wamelen]

In big_operators there is a sum_smul' lemma:

lemma sum_smul' [add_comm_monoid β] (s : finset α) (n : ℕ) (f : α → β) :
  (∑ x in s, add_monoid.smul n (f x)) = add_monoid.smul n ((∑ x in s, f x)) :=
@prod_pow _ (multiplicative β) _ _ _ _
attribute [to_additive sum_smul'] prod_pow

Why can't I seem to use this lemma? I get unknown identifier 'sum_smul'' even later in the big_operators file?
Probably related: Is there somewhere I can read up on to_additive?

[Jalex Stark]

did you open the right namespace?

[Mario Carneiro]

it's probably in the finset namespace

[Mario Carneiro]

https://leanprover-community.github.io/mathlib_docs/algebra/group/to_additive.html

[Paul van Wamelen]

Thanks and thanks! Yeah finset.sum_smul' does the trick.

[Kevin Buzzard]

Typing #where just after a definition will tell you the name of the namespace you're in when you made it.

Unfortunately editing mathlib can cause recompilation issues.

It's a shame that we can't hover over a definition and see exactly what we see when we hover over a use of that definition.

[Paul van Wamelen]

Oh, this is good to know!

[Alex Zhang]

@[to_additive]
lemma mul_smul_comm [has_mul α] (s : M) (x y : α) [smul_comm_class M α α] :
  x * (s • y) = s • (x * y) :=
(smul_comm s x y).symm

[Alex Zhang]

If my understanding is correct, @[to_additive] allows me to change * to +. But how can I use this feature?

[Ruben Van de Velde]

There will be another lemma, docs#add_vadd_comm that you can use instead

[Alex Zhang]

Do you mean @[to_additive] automatically produces another lemma add_vadd_comm?

[Ruben Van de Velde]

Yep

[Alex Zhang]

How the name add_vadd_comm is determined?

[Alex Zhang]

Namely, how do I know what the lemmas that @[to_additive] produces are?

[Ruben Van de Velde]

The easiest way is to go to docs#mul_smul_comm and scroll up - the last lemma or definition before the multiplicative version is the additive version

[Alex Zhang]

I don't quite understand how @[to_additive] works or what it allows us to do.

[Alex Zhang]

By the way, what does v stand for in vadd?

[Anne Baanen]

Alex Zhang said:

I don't quite understand how @[to_additive] works or what it allows us to do.

When you add a @[to_additive] annotation to a declaration (def or theorem), it calls a tactic that automatically generates a copy of that declaration. In this copy, all references to multiplicative structure (mul, one, inv) are replaced with additive structures (add, zero, neg). You can think of it as copy-pasting the declaration and find-and-replace mul with add, one with zero, inv with neg, except smarter.