Commit 2024-01-23 19:39 a5d2da9f

View on Github →

refactor(Data/Rat/NNRat): move BigOperator lemmas to a new file (#9917) NNRat has far too many dependencies at the moment. This only removes 20 from its transitive closure (1609 -> 1589 according to lake exe graph and | wc -l), but it's a start.

Estimated changes

deleted theorem NNRat.coe_list_prod
deleted theorem NNRat.coe_list_sum
deleted theorem NNRat.coe_multiset_prod
deleted theorem NNRat.coe_multiset_sum
deleted theorem NNRat.coe_prod
deleted theorem NNRat.coe_sum