Binomial theorem

Stream: Is there code for X?

[Julian Sutherland]

Is the binomial theorem encoded somewhere in mathlib?

[Oliver Nash]

Yes, various versions. See e.g., docs#commute.add_pow

A good way to search for things like this is to use the search box in the top right here https://leanprover-community.github.io/mathlib_docs/

[Julian Sutherland]

@Oliver Nash Thank you! I gave that a try, however, wasn't able to find it with any key words involving the word "binomial".

[Oliver Nash]

How odd, here's what I see (before even clicking anything):

[Oliver Nash]

image.png

[Julian Sutherland]

@Oliver Nash Fair enough, the name just didn't strike me, so I didn't have a look, my fault entirely!

[Oliver Nash]

Certainly not your fault. Just a little tip that somebody once told me.

[Yaël Dillies]

It certainly is a bit surprising at first that the search is not only performed on what we see (the lemma name) but also on what we don't (the docstring).

[Martin Dvořák]

Oliver Nash said:

Yes, various versions. See e.g., docs#commute.add_pow

A good way to search for things like this is to use the search box in the top right here https://leanprover-community.github.io/mathlib_docs/

Why does it even hold for non-commutative semirings? Say n = 2. How do you go from x^2 + x*y + y*x + y^2 to x^2 + x*y*2 + y^2 here?

[Kevin Buzzard]

It holds if x and y commute.

[Martin Dvořák]

Oh I see now!

variables [semiring R] {x y : R} (h : commute x y) (n : ℕ)

include h

/-- A version of the **binomial theorem** for noncommutative semirings. -/
theorem add_pow :
  (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=

[Martin Dvořák]

My belief that explicit arguments should not be taken out of the declaration and stored in variables has been further reinforced.

[Johan Commelin]

Hmm, I would rather say that include is almost always evil. (But sometimes convenient.)

[Johan Commelin]

variables is fine, but include is a bit of a code smell.

[Martin Dvořák]

At certain points, I decided to never use variables for explicit arguments and refactored my code accordingly.

[Martin Dvořák]

Basically variables (anything) is a no-go.

[Yaël Dillies]

In that case, everything is in the commute namespace, so everything takes a commute x y assumption.

[Martin Dvořák]

I understand what it does. I am just saying I was feeling very uncomfortable from locally reading

/-- A version of the **binomial theorem** for noncommutative semirings. -/
theorem add_pow :
  (x + y) ^ n = ∑ m in range (n + 1), x ^ m * y ^ (n - m) * choose n m :=

and not being able to make sense of it.

[Kevin Buzzard]

In lean 4 the fact that you're in the commute namespace is indicated in the breadcrumbs

[Johan Commelin]

But that's no more than a hint, right? I agree with @Martin Dvořák that it would be nice to see commute x y explicitly in that statement.

[Reid Barton]

I think maybe this depends on how much you use explicit arguments in general. Like if you want to make x and y explicit in add_comm x y, then you won't want to write x y in every theorem statement.

[Johan Commelin]

Yep, so I'm not against variables (x y : A) at all. I just think that include is often suspicious.

[Floris van Doorn]

I think explicit arguments that are mentioned in a lemma statement are fine to put in variables.
It is a nicer style to write arguments that are not mentioned in the lemma statement (usually hypotheses/side conditions) explicitly for each lemma (this usually requires an include, but not always).

[Martin Dvořák]

Some time ago, we had a similar discussion and most of us afair agreed on writing explicit arguments explicitly for each declaration.

[Heather Macbeth]

An advantage of keeping them out in a variables line is that it standardizes argument order across similar lemmas.

[Heather Macbeth]

Look at the core analysis files for this in practice, e.g.
https://github.com/leanprover-community/mathlib/blob/ed005a8c91df8f75bf3a92255114659c2dad9907/src/analysis/calculus/fderiv.lean#L185

[Martin Dvořák]

Only one of them is explicit here. Hence standardizing their order doesn't bring much to the table.

[Martin Dvořák]

https://github.com/leanprover-community/mathlib/pull/18071