Commit 2025-07-05 03:31 fb02731f

View on Github →

chore(Algebra/BigOperators): rename variables away from greek letters (#26521) Uniformise the variables to ι, κ for the indexing types, M, N for monoids, G for groups, M₀ for monoids with zero, R for (semi)rings. Also delete a duplicated lemma which suddenly became problematic.

Estimated changes

modified theorem Associates.finset_prod_mk
modified theorem Associates.prod_eq_one_iff
modified theorem Associates.prod_le_prod
modified theorem Associates.prod_mk
modified theorem Finset.prod_primes_dvd
modified theorem Multiset.prod_primes_dvd
modified theorem Prime.dvd_finset_prod_iff
modified theorem Prime.dvd_finsuppProd_iff
modified theorem Prime.exists_mem_finset_dvd
modified theorem Prime.not_dvd_finset_prod
modified theorem Prime.not_dvd_finsuppProd
modified theorem divisor_closure_eq_closure
modified def Fin.partialProd
modified theorem Fin.partialProd_succ'
modified theorem Fin.partialProd_succ
modified theorem Fin.partialProd_zero
modified theorem Fin.prod_univ_fun_getElem
modified theorem Fin.prod_univ_two'
modified theorem List.prod_ofFn
modified theorem List.prod_take_ofFn
modified theorem Equiv.Perm.prod_comp'
modified theorem Equiv.Perm.prod_comp
modified theorem Equiv.prod_comp
modified theorem Finset.ite_one_prod
modified theorem Finset.ite_prod_one
modified theorem Finset.op_sum
modified theorem Finset.prod_attach_univ
modified theorem Finset.prod_const_one
modified theorem Finset.prod_dite_irrel
modified theorem Finset.prod_div_distrib
modified theorem Finset.prod_erase_attach
modified theorem Finset.prod_hom_rel
modified theorem Finset.prod_induction
modified theorem Finset.prod_int_mod
modified theorem Finset.prod_inv_distrib
modified theorem Finset.prod_ite_index
modified theorem Finset.prod_ite_irrel
modified theorem Finset.prod_map
modified theorem Finset.prod_map_toList
modified theorem Finset.prod_map_val
modified theorem Finset.prod_mem_multiset
modified theorem Finset.prod_mk
modified theorem Finset.prod_nat_mod
modified theorem Finset.prod_of_isEmpty
modified theorem Finset.prod_pow
modified theorem Finset.prod_range_zero
modified theorem Finset.prod_toList
modified theorem Finset.prod_val
modified theorem Finset.prod_zpow
modified theorem Finset.sum_int_mod
modified theorem Finset.sum_nat_mod
modified theorem Finset.unop_sum
modified theorem Fintype.prod_bijective
modified theorem Fintype.prod_empty
modified theorem Fintype.prod_equiv
modified theorem Multiset.count_sum'
modified theorem Units.coe_prod
modified theorem map_prod
modified theorem ofAdd_list_prod
modified theorem ofAdd_multiset_prod
modified theorem ofAdd_sum
modified theorem ofMul_list_prod
modified theorem ofMul_multiset_prod
modified theorem ofMul_prod
modified theorem toAdd_list_sum
modified theorem toAdd_multiset_sum
modified theorem toAdd_prod
modified theorem toMul_list_sum
modified theorem toMul_multiset_sum
modified theorem toMul_sum
modified theorem Finset.isSquare_prod
modified theorem Finset.mulSupport_prod
modified theorem MonoidHom.coe_finset_prod
modified theorem MonoidHom.finset_prod_apply
modified theorem Finset.dvd_prod_of_mem
modified theorem Finset.prod_apply_dite
modified theorem Finset.prod_apply_ite
modified theorem Finset.prod_dite
modified theorem Finset.prod_dite_eq'
modified theorem Finset.prod_dite_eq
modified theorem Finset.prod_dite_of_false
modified theorem Finset.prod_dite_of_true
modified theorem Finset.prod_ite
modified theorem Finset.prod_ite_eq'
modified theorem Finset.prod_ite_eq
modified theorem Finset.prod_ite_eq_of_mem'
modified theorem Finset.prod_ite_eq_of_mem
modified theorem Finset.prod_ite_mem
modified theorem Finset.prod_ite_of_false
modified theorem Finset.prod_ite_of_true
modified theorem Finset.prod_ite_one
modified theorem Finset.prod_pi_mulSingle'
modified theorem Finset.prod_pi_mulSingle
modified theorem Finset.prod_piecewise
modified theorem Finset.prod_pow_boole
modified theorem Finset.prod_update_of_mem
modified theorem Fintype.prod_dite_eq'
modified theorem Fintype.prod_dite_eq
modified theorem Fintype.prod_ite_eq'
modified theorem Fintype.prod_ite_eq
modified theorem Fintype.prod_ite_mem
modified theorem Fintype.prod_pi_mulSingle'
modified theorem Fintype.prod_pi_mulSingle
modified theorem List.alternatingProd_cons
modified theorem List.alternatingProd_nil
modified theorem List.prod_map_mul
modified theorem List.prod_isUnit_iff
modified theorem Multiset.fst_prod
modified theorem Multiset.prod_add
modified theorem Multiset.prod_eq_one
modified theorem Multiset.prod_eq_pow_single
modified theorem Multiset.prod_erase
modified theorem Multiset.prod_hom'
modified theorem Multiset.prod_hom
modified theorem Multiset.prod_hom_ne_zero
modified theorem Multiset.prod_hom₂
modified theorem Multiset.prod_map_inv'
modified theorem Multiset.prod_map_prod_map
modified theorem Multiset.prod_nsmul
modified theorem Multiset.snd_prod
modified theorem Multiset.sum_map_singleton
modified theorem Multiset.sum_map_tsub
modified theorem map_multiset_ne_zero_prod
modified theorem map_multiset_prod
modified theorem Multiset.pow_count
modified def Multiset.prod
modified theorem Multiset.prod_coe
modified theorem Multiset.prod_cons
modified theorem Multiset.prod_eq_foldl
modified theorem Multiset.prod_eq_foldr
modified theorem Multiset.prod_hom_rel
modified theorem Multiset.prod_induction
modified theorem Multiset.prod_map_one
modified theorem Multiset.prod_pair
modified theorem Multiset.prod_replicate
modified theorem Multiset.prod_singleton
modified theorem Multiset.prod_toList
modified theorem Multiset.prod_zero
modified theorem Finset.smul_prod'
modified theorem Finset.smul_prod_perm
modified theorem Finset.smul_sum
modified theorem List.smul_prod'
modified theorem List.smul_prod
modified theorem List.smul_sum
modified theorem Multiset.smul_prod'
modified theorem Multiset.smul_prod
modified theorem Multiset.smul_sum
modified theorem smul_finprod'
modified theorem smul_finprod_perm
modified theorem smul_finsum_mem
modified theorem Finset.prod_apply
modified theorem Finset.prod_fn
modified theorem Finset.univ_prod_mulSingle
modified theorem Fintype.prod_apply
modified theorem MonoidHom.functions_ext'
modified theorem MonoidHom.functions_ext
modified theorem Pi.list_prod_apply
modified theorem Pi.multiset_prod_apply
modified theorem RingHom.functions_ext
modified theorem prod_indicator
modified theorem prod_indicator_apply
modified theorem prod_indicator_const
modified theorem prod_indicator_const_apply
modified theorem prod_mk_prod
modified theorem Commute.sum_left
modified theorem Commute.sum_right
modified theorem Finset.mul_sum
modified theorem Finset.prod_add
modified theorem Finset.prod_add_one
modified theorem Finset.prod_add_ordered
modified theorem Finset.prod_add_prod_eq
modified theorem Finset.prod_natCast
modified theorem Finset.prod_neg
modified theorem Finset.prod_one_add
modified theorem Finset.prod_one_sub_ordered
modified theorem Finset.prod_sub
modified theorem Finset.prod_sub_ordered
modified theorem Finset.prod_sum
modified theorem Finset.prod_univ_sum
modified theorem Finset.sum_boole_mul
modified theorem Finset.sum_mul
modified theorem Finset.sum_mul_boole
modified theorem Finset.sum_mul_sum
modified theorem Finset.sum_pow'
modified theorem Finset.sum_prod_piFinset
modified theorem Fintype.prod_add
modified theorem Fintype.prod_sum
modified theorem Fintype.sum_mul_sum
modified theorem Fintype.sum_pow
modified theorem Int.cast_list_prod
modified theorem Int.cast_list_sum
modified theorem Int.cast_multiset_sum
modified theorem Int.cast_prod
modified theorem Int.cast_sum
modified theorem Nat.cast_list_prod
modified theorem Nat.cast_list_sum
modified theorem Nat.cast_multiset_prod
modified theorem Nat.cast_multiset_sum
modified theorem Nat.cast_prod
modified theorem Nat.cast_sum
modified theorem Commute.multiset_sum_left
modified theorem Commute.multiset_sum_right
modified theorem Multiset.prod_eq_zero
modified theorem Multiset.prod_eq_zero_iff
modified theorem Multiset.prod_map_add
modified theorem Multiset.prod_map_neg
modified theorem Multiset.prod_map_sum
modified theorem Multiset.prod_ne_zero
modified theorem WithBot.bot_lt_prod
modified theorem WithBot.coe_sum
modified theorem WithTop.coe_sum
modified theorem WithTop.prod_lt_top