Commit 2020-05-15 03:11 378aa0d7
View on Github →feat(data/nat/choose): Sum a row of Pascal's triangle (#2684) Add the "sum of the nth row of Pascal's triangle" theorem. Naming is hard, of course, and this is my first PR to mathlib, so naming suggestions are welcome. Briefly discussed at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Candidate.20for.20inclusion.20in.20mathlib/near/197619403 .