mathlib3
2a04ec03 - feat(data/list/big_operators): More lemmas about alternating product (#13195)

Commit
4 years ago
feat(data/list/big_operators): More lemmas about alternating product (#13195) A few more lemmas about `list.alternating_prod` and `list.alternating_sum` and a proof that 11 divides even length base 10 palindromes. Also rename `palindrome` to `list.palindrome` (as it should have been). Co-authored-by: Chris Wong Co-authored-by: Chris Wong <lambda.fairy@gmail.com>
Author
Parents
Loading