Commit 2023-01-10 07:36 68d8ac54

View on Github →

feat: port Data.List.BigOperators.Basic (#1380)

Initial file copy from mathport
Mathbin -> Mathlib; add import to Mathlib.lean

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/List/BigOperators/Basic.lean

added theorem Commute.list_prod_left

added theorem Commute.list_prod_right

added theorem List.Forall₂.prod_le_prod'

added theorem List.Sublist.prod_le_prod'

added theorem List.SublistForall₂.prod_le_prod'

added theorem List.all_one_of_le_one_le_of_prod_eq_one

added theorem List.alternating_prod_cons'

added theorem List.alternating_prod_cons

added theorem List.alternating_prod_cons_cons'

added theorem List.alternating_prod_cons_cons

added theorem List.alternating_prod_nil

added theorem List.alternating_prod_singleton

added theorem List.eq_of_prod_take_eq

added theorem List.exists_le_of_prod_le'

added theorem List.exists_lt_of_prod_lt'

added theorem List.exists_mem_ne_one_of_prod_ne_one

added theorem List.get?_zero_mul_tail_prod

added theorem List.headI_add_tail_sum

added theorem List.headI_le_sum

added theorem List.headI_mul_tail_prod_of_ne_nil

added theorem List.length_pos_of_one_lt_prod

added theorem List.length_pos_of_prod_lt_one

added theorem List.length_pos_of_prod_ne_one

added theorem List.monotone_prod_take

added theorem List.one_le_prod_of_one_le

added theorem List.one_lt_prod_of_one_lt

added theorem List.prod_append

added theorem List.prod_concat

added theorem List.prod_cons

added theorem List.prod_drop_succ

added theorem List.prod_eq_foldr

added theorem List.prod_eq_one

added theorem List.prod_eq_pow_card

added theorem List.prod_eq_zero

added theorem List.prod_eq_zero_iff

added theorem List.prod_erase

added theorem List.prod_hom

added theorem List.prod_hom_rel

added theorem List.prod_hom₂

added theorem List.prod_inv

added theorem List.prod_inv_reverse

added theorem List.prod_isUnit

added theorem List.prod_isUnit_iff

added theorem List.prod_join

added theorem List.prod_le_pow_card

added theorem List.prod_le_prod'

added theorem List.prod_lt_prod'

added theorem List.prod_lt_prod_of_ne_nil

added theorem List.prod_map_erase

added theorem List.prod_map_hom

added theorem List.prod_map_mul

added theorem List.prod_map_neg

added theorem List.prod_ne_zero

added theorem List.prod_nil

added theorem List.prod_pos

added theorem List.prod_repeat

added theorem List.prod_replicate

added theorem List.prod_reverse_noncomm

added theorem List.prod_set'

added theorem List.prod_set

added theorem List.prod_singleton

added theorem List.prod_take_mul_prod_drop

added theorem List.prod_take_succ

added theorem List.single_le_prod

added theorem List.sum_const_nat

added theorem List.sum_le_foldr_max

added theorem List.tail_sum

added theorem map_list_prod