Commit 2022-11-30 07:27 23f67f2f

View on Github →

chore(data/rat/cast): split (#17761) Split off data/rat/big_operators from data/rat/cast, removing the algebra/big_operators/basic import (and, as a consequence, finset) from the latter.

Estimated changes

Modified src/algebra/module/basic.lean

Modified src/data/bitvec/basic.lean

Modified src/data/finset/sym.lean

Modified src/data/finsupp/basic.lean

Created src/data/rat/big_operators.lean

added theorem rat.cast_list_prod

added theorem rat.cast_list_sum

added theorem rat.cast_multiset_prod

added theorem rat.cast_multiset_sum

added theorem rat.cast_prod

added theorem rat.cast_sum

Modified src/data/rat/cast.lean

deleted theorem rat.cast_list_prod

deleted theorem rat.cast_list_sum

deleted theorem rat.cast_multiset_prod

deleted theorem rat.cast_multiset_sum

deleted theorem rat.cast_prod

deleted theorem rat.cast_sum

Modified src/data/sym/sym2.lean

Modified src/tactic/norm_fin.lean

Modified src/tactic/omega/clause.lean

Modified src/tactic/ring.lean

Modified src/testing/slim_check/gen.lean

Modified test/induction.lean