cast}): Missing cast lemmas (#14824)

Commit

3 years ago

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.

Author

YaelDillies

Parents

38642efc

mathlib 44bb35e5 - feat({algebra/big_operators/basic,data/rat/cast}): Missing cast lemmas (#14824)

mathlib
44bb35e5 - feat({algebra/big_operators/basic,data/rat/cast}): Missing cast lemmas (#14824)