Commit 2025-04-19 14:06 9bc7ea29

View on Github →

chore(Algebra/BigOperators/Group/Finset/Basic): use meaningful letter names (#24123) All monoids are M, all groups are G, all indexing types are ι or κ. Also order according to typeclass assumptions

Estimated changes

modified theorem Finset.card_biUnion
modified theorem Finset.card_biUnion_le
modified theorem Finset.card_disjiUnion
modified theorem Finset.card_eq_sum_ones
modified theorem Finset.eq_prod_range_div'
modified theorem Finset.eq_prod_range_div
modified theorem Finset.mem_sum
modified theorem Finset.mul_prod_erase
modified theorem Finset.pow_card_mul_prod
modified theorem Finset.pow_eq_prod_const
modified theorem Finset.prod_attach
modified theorem Finset.prod_biUnion
modified theorem Finset.prod_bij_ne_one
modified theorem Finset.prod_comp
modified theorem Finset.prod_compl_mul_prod
modified theorem Finset.prod_congr_set
modified theorem Finset.prod_const
modified theorem Finset.prod_diag
modified theorem Finset.prod_disj_sum
modified theorem Finset.prod_disjiUnion
modified theorem Finset.prod_dvd_prod_of_dvd
modified theorem Finset.prod_eq_fold
modified theorem Finset.prod_eq_mul
modified theorem Finset.prod_eq_mul_of_mem
modified theorem Finset.prod_eq_one
modified theorem Finset.prod_eq_one_iff
modified theorem Finset.prod_eq_pow_card
modified theorem Finset.prod_eq_prod_extend
modified theorem Finset.prod_eq_single
modified theorem Finset.prod_erase
modified theorem Finset.prod_erase_eq_div
modified theorem Finset.prod_erase_mul
modified theorem Finset.prod_extend_by_one
modified theorem Finset.prod_fiberwise'
modified theorem Finset.prod_fiberwise
modified theorem Finset.prod_filter
modified theorem Finset.prod_filter_ne_one
modified theorem Finset.prod_filter_of_ne
modified theorem Finset.prod_filter_xor
modified theorem Finset.prod_finset_coe
modified theorem Finset.prod_flip
modified theorem Finset.prod_image'
modified theorem Finset.prod_image
modified theorem Finset.prod_insert
modified theorem Finset.prod_insert_div
modified theorem Finset.prod_insert_one
modified theorem Finset.prod_involution
modified theorem Finset.prod_list_count
modified theorem Finset.prod_list_map_count
modified theorem Finset.prod_mul_pow_card
modified theorem Finset.prod_mul_prod_comm
modified theorem Finset.prod_mul_prod_compl
modified theorem Finset.prod_multiset_count
modified theorem Finset.prod_ninvolution
modified theorem Finset.prod_pair
modified theorem Finset.prod_partition
modified theorem Finset.prod_pow_eq_pow_sum
modified theorem Finset.prod_range_add
modified theorem Finset.prod_range_div'
modified theorem Finset.prod_range_div
modified theorem Finset.prod_range_induction
modified theorem Finset.prod_range_one
modified theorem Finset.prod_range_succ'
modified theorem Finset.prod_range_succ
modified theorem Finset.prod_range_succ_comm
modified theorem Finset.prod_sdiff
modified theorem Finset.prod_sdiff_eq_div
modified theorem Finset.prod_set_coe
modified theorem Finset.prod_singleton
modified theorem Finset.prod_subtype
modified theorem Finset.prod_subtype_of_mem
modified theorem Finset.prod_sumElim
modified theorem Finset.prod_union
modified theorem Finset.prod_union_eq_left
modified theorem Finset.prod_union_eq_right
modified theorem Finset.prod_union_inter
modified theorem Finset.prod_unique_nonempty
modified theorem Finset.sum_const_nat
modified theorem Finset.sum_range_tsub
modified theorem Finset.sum_tsub_distrib
modified theorem Fintype.prod_Prop
modified theorem Fintype.prod_fiberwise'
modified theorem Fintype.prod_fiberwise
modified theorem Fintype.prod_of_injective
modified theorem Fintype.prod_subset
modified theorem Fintype.prod_subsingleton
modified theorem Fintype.prod_unique
modified theorem IsCompl.prod_mul_prod
modified theorem IsUnit.prod_iff
modified theorem IsUnit.prod_univ_iff
modified theorem List.prod_toFinset
modified theorem Multiset.mem_sum
modified theorem Multiset.prod_sum
modified theorem Multiset.sum_count_eq_card
modified theorem nat_abs_sum_le