Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-09 00:02 2a04ec03

View on Github →

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).

Estimated changes

Modified src/data/list/big_operators.lean

added theorem list.alternating_prod_append

added theorem list.alternating_prod_cons'

added theorem list.alternating_prod_cons

added theorem list.alternating_prod_cons_cons'

modified theorem list.alternating_prod_cons_cons

modified theorem list.alternating_prod_nil

added theorem list.alternating_prod_reverse

modified theorem list.alternating_prod_singleton

deleted theorem list.alternating_sum_cons_cons

Modified src/data/list/palindrome.lean

added theorem list.palindrome.append_reverse

added theorem list.palindrome.iff_reverse_eq

added theorem list.palindrome.of_reverse_eq

added theorem list.palindrome.reverse_eq

added inductive list.palindrome

deleted theorem palindrome.append_reverse

deleted theorem palindrome.iff_reverse_eq

deleted theorem palindrome.of_reverse_eq

deleted theorem palindrome.reverse_eq

deleted inductive palindrome

Modified src/data/nat/digits.lean

modified theorem nat.eleven_dvd_iff

added theorem nat.eleven_dvd_of_palindrome