Commit 2021-10-24 22:52 12515db6

View on Github →

feat(data/list): product of list.update_nth in terms of inverses (#9800) Expression for the product of l.update_nth n x in terms of inverses instead of take and drop, assuming a group instead of a monoid.

Estimated changes

Modified src/data/list/basic.lean

added theorem list.prod_drop_succ

added theorem list.prod_update_nth'

deleted theorem list.sum_take_add_sum_drop

deleted theorem list.sum_take_succ

Modified src/data/list/zip.lean

added theorem list.prod_mul_prod_eq_prod_zip_with_mul_prod_drop

added theorem list.prod_mul_prod_eq_prod_zip_with_of_length_eq

Modified src/data/vector/basic.lean

added theorem vector.prod_update_nth'

added theorem vector.prod_update_nth

added theorem vector.to_list_update_nth

Modified src/data/vector/zip.lean

added theorem vector.prod_mul_prod_eq_prod_zip_with