[Merged by Bors] - feat(algebra/indicator_function): smul lemmas for functions

[sgouezel]

And a few basic lemmas in set/basic.

---

[eric-wieser]

I think the original name derives from:

lemma indicator_smul' (s : set α) (r : M) (f : α → A) (x : α) :
  indicator s (r • f) x = r • indicator s f x :=

(which matches indicator_one' and some other primed lemmas above)

[sgouezel]

I don't understand your comment, because I can't locate the lemma indicator_smul' you mention. But if you have suggestions for better names, I'll take your word on it because you're probably more familiar with this part of the library than I am.

[eric-wieser]

Apologies. My comment amounts to:

• We should have indicator_smul' as a lemma (it doesn't exist right now)
• The difference between indicator_mul and indicator_mul' suggests that the lemma this comment is on already has the expected name.

However, I don't see a better name for the new lemma than what you already have.
I think @urkud is more familiar than me, so I'm happy to defer to their opinion.

[urkud]

It was named smul because there was no other version. Am I right that the old lemma follows from the new lemma? Do we need the old lemma once we have the new one?

[sgouezel]

The old lemmas indeed follow from the new ones, so I've exchanged their order in the file to golf their proofs. However, they are still needed in the library as rw and simp struggle with the function lemmas in the constant case. So, I am keeping them.

[urkud]

Thanks!
bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests