Commit 2025-01-10 04:57 07f59252

View on Github →

chore: split Algebra/BigOperators/Group/List (#20625)

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/Algebra/BigOperators/Group/List.lean to Mathlib/Algebra/BigOperators/Group/List/Basic.lean

deleted theorem List.Perm.prod_eq'

deleted theorem List.Sublist.prod_dvd_prod

deleted def List.alternatingProd

deleted theorem List.alternatingProd_append

deleted theorem List.alternatingProd_reverse

deleted def List.alternatingSum

deleted theorem List.drop_take_succ_flatten_eq_getElem

deleted theorem List.drop_take_succ_join_eq_get

deleted theorem List.dvd_prod

deleted theorem List.length_sigma

deleted theorem List.mem_mem_ranges_iff_lt_sum

deleted theorem List.neg_one_mem_of_prod_eq_neg_one

deleted def List.prod

deleted theorem List.prod_cons

deleted theorem List.prod_eq_foldr

deleted theorem List.prod_eq_pow_card

deleted theorem List.prod_hom_rel

deleted theorem List.prod_induction

deleted theorem List.prod_isUnit

deleted theorem List.prod_isUnit_iff

deleted theorem List.prod_map_one

deleted theorem List.prod_nil

deleted theorem List.prod_one_cons

deleted theorem List.prod_replicate

deleted theorem List.prod_rotate_eq_one_of_prod_eq_one

deleted theorem List.prod_singleton

deleted theorem List.ranges_flatten

deleted theorem List.ranges_nodup

deleted theorem List.sum_map_count_dedup_eq_length

deleted theorem List.sum_map_count_dedup_filter_eq_countP

deleted theorem MulOpposite.op_list_prod

deleted theorem MulOpposite.unop_list_prod

deleted theorem unop_map_list_prod

Created Mathlib/Algebra/BigOperators/Group/List/Defs.lean

added def List.alternatingProd

added def List.alternatingSum

added def List.prod

added theorem List.prod_cons

added theorem List.prod_eq_foldr

added theorem List.prod_eq_pow_card

added theorem List.prod_hom_rel

added theorem List.prod_induction

added theorem List.prod_map_one

added theorem List.prod_nil

added theorem List.prod_one_cons

added theorem List.prod_replicate

added theorem List.prod_singleton

Created Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean

added theorem List.Perm.prod_eq'

added theorem List.Sublist.prod_dvd_prod

added theorem List.alternatingProd_append

added theorem List.alternatingProd_reverse

added theorem List.drop_take_succ_flatten_eq_getElem

added theorem List.drop_take_succ_join_eq_get

added theorem List.dvd_prod

added theorem List.length_sigma

added theorem List.mem_mem_ranges_iff_lt_sum

added theorem List.neg_one_mem_of_prod_eq_neg_one

added theorem List.prod_isUnit

added theorem List.prod_isUnit_iff

added theorem List.prod_rotate_eq_one_of_prod_eq_one

added theorem List.ranges_flatten

added theorem List.ranges_nodup

added theorem List.sum_map_count_dedup_eq_length

added theorem List.sum_map_count_dedup_filter_eq_countP

added theorem MulOpposite.op_list_prod

added theorem MulOpposite.unop_list_prod

added theorem unop_map_list_prod

Modified Mathlib/Algebra/BigOperators/Group/Multiset.lean

Modified Mathlib/Algebra/BigOperators/Ring/List.lean

Modified Mathlib/Algebra/FreeMonoid/Basic.lean

Modified Mathlib/Algebra/GradedMonoid.lean

Modified Mathlib/Algebra/Group/Pointwise/Set/ListOfFn.lean

Modified Mathlib/Algebra/Order/BigOperators/Group/List.lean

Modified Mathlib/Algebra/Order/BigOperators/GroupWithZero/List.lean

Modified Mathlib/Algebra/Order/BigOperators/Ring/List.lean

Modified Mathlib/Data/List/Prime.lean

Modified Mathlib/Data/Vector/Basic.lean

Modified Mathlib/GroupTheory/Congruence/BigOperators.lean

Modified Mathlib/GroupTheory/FreeGroup/Basic.lean

Modified scripts/noshake.json