Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-22 18:31 44bb35e5

View on Github →

feat({algebra/big_operators/basic,data/rat/cast}): Missing cast lemmas (#14824) rat.cast_sum, rat.cast_prod and nat, int lemmas about multiset and list big operators.

Estimated changes

added theorem int.cast_list_prod
added theorem int.cast_list_sum
added theorem int.cast_multiset_prod
added theorem int.cast_multiset_sum
modified theorem int.cast_prod
modified theorem int.cast_sum
added theorem nat.cast_list_prod
added theorem nat.cast_list_sum
added theorem nat.cast_multiset_prod
added theorem nat.cast_multiset_sum
modified theorem nat.cast_prod
modified theorem nat.cast_sum
added theorem rat.cast_finsupp_prod
added theorem rat.cast_finsupp_sum
modified theorem rat.cast_div
modified def rat.cast_hom
modified theorem rat.cast_inv
added theorem rat.cast_list_prod
added theorem rat.cast_list_sum
modified theorem rat.cast_mk
added theorem rat.cast_multiset_prod
added theorem rat.cast_multiset_sum
modified theorem rat.cast_pow
added theorem rat.cast_prod
added theorem rat.cast_sum
modified theorem rat.coe_cast_hom