Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-14 05:19 ad0988b3

View on Github →

docs(algebra/*): Add docstrings to additive lemmas (#12578) Many additive lemmas had no docstrings while their multiplicative counterparts had. This adds them in all files under algebra.

Estimated changes

modified theorem finset.prod_ite_eq'
deleted theorem finset.sum_comp
modified theorem finprod_comp
modified theorem finprod_div_distrib
modified theorem finprod_emb_domain'
modified theorem finprod_eq_of_bijective
modified theorem finprod_induction
modified theorem finprod_mem_Union
modified theorem finprod_mem_bUnion
modified theorem finprod_mem_comm
modified theorem finprod_mem_div_distrib
modified theorem finprod_mem_dvd
modified theorem finprod_mem_empty
modified theorem finprod_mem_eq_of_bij_on
modified theorem finprod_mem_finset_product'
modified theorem finprod_mem_finset_product
modified theorem finprod_mem_image'
modified theorem finprod_mem_image
deleted theorem finprod_mem_induction
modified theorem finprod_mem_insert'
modified theorem finprod_mem_insert
modified theorem finprod_mem_insert_one
modified theorem finprod_mem_mul_diff'
modified theorem finprod_mem_mul_diff
modified theorem finprod_mem_mul_distrib'
modified theorem finprod_mem_mul_distrib
modified theorem finprod_mem_of_eq_on_one
modified theorem finprod_mem_one
modified theorem finprod_mem_pair
modified theorem finprod_mem_range'
modified theorem finprod_mem_range
modified theorem finprod_mem_sUnion
modified theorem finprod_mem_singleton
modified theorem finprod_mem_union''
modified theorem finprod_mem_union'
modified theorem finprod_mem_union
deleted theorem finprod_mem_union_inter'
modified theorem finprod_mem_union_inter
modified theorem finprod_mul_distrib
modified theorem finsum_mul
modified theorem finsum_smul
modified theorem monoid_hom.map_finprod_mem'
modified theorem monoid_hom.map_finprod_mem
modified theorem mul_finsum
modified theorem commute.mul_left
modified theorem commute.mul_right
modified theorem map_div
modified theorem semiconj_by.conj_mk
modified theorem semiconj_by.mul_left
modified theorem semiconj_by.mul_right
modified theorem semiconj_by.units_inv_right
modified theorem abs_eq_sup_inv