Commit 2023-01-23 14:15 98746efc

View on Github →

feat: port Algebra.BigOperators.Finprod (#1766) Some mathport warnings in here that I left in for the experts to review. Rest should be done!

Estimated changes

added theorem MonoidHom.map_finprod
added theorem MulEquiv.map_finprod
added theorem finprod_comp
added theorem finprod_comp_equiv
added theorem finprod_cond_eq_left
added theorem finprod_cond_eq_right
added theorem finprod_cond_ne
added theorem finprod_cond_nonneg
added theorem finprod_congr
added theorem finprod_congr_Prop
added theorem finprod_curry
added theorem finprod_curry₃
added theorem finprod_def
added theorem finprod_div_distrib
added theorem finprod_dmem
added theorem finprod_emb_domain'
added theorem finprod_emb_domain
added theorem finprod_eq_dif
added theorem finprod_eq_if
added theorem finprod_eq_prod
added theorem finprod_eq_single
added theorem finprod_eq_zero
added theorem finprod_false
added theorem finprod_induction
added theorem finprod_inv_distrib
added theorem finprod_mem_bunionᵢ
added theorem finprod_mem_coe_finset
added theorem finprod_mem_comm
added theorem finprod_mem_congr
added theorem finprod_mem_def
added theorem finprod_mem_dvd
added theorem finprod_mem_empty
added theorem finprod_mem_eq_prod
added theorem finprod_mem_image'
added theorem finprod_mem_image
added theorem finprod_mem_induction
added theorem finprod_mem_insert'
added theorem finprod_mem_insert
added theorem finprod_mem_insert_one
added theorem finprod_mem_mulSupport
added theorem finprod_mem_mul_diff'
added theorem finprod_mem_mul_diff
added theorem finprod_mem_one
added theorem finprod_mem_pair
added theorem finprod_mem_range'
added theorem finprod_mem_range
added theorem finprod_mem_singleton
added theorem finprod_mem_union''
added theorem finprod_mem_union'
added theorem finprod_mem_union
added theorem finprod_mem_unionᵢ
added theorem finprod_mem_unionₛ
added theorem finprod_mem_univ
added theorem finprod_mul_distrib
added theorem finprod_nonneg
added theorem finprod_of_isEmpty
added theorem finprod_one
added theorem finprod_pow
added theorem finprod_prod_comm
added theorem finprod_true
added theorem finprod_unique
added theorem finsum_mul
added theorem finsum_smul
added theorem mul_finprod_cond_ne
added theorem mul_finsum
added theorem one_le_finprod'
added theorem prod_finprod_comm
added theorem single_le_finprod
added theorem smul_finsum