Commit 2023-08-25 07:09 3672fba8
View on Github →feat: add some lemmas about Finsupp.indicator (#6719)
It's hard to rewrite after using indicator_eq_sum_single and prod_indicator_index, so I add these two lemmas.
feat: add some lemmas about Finsupp.indicator (#6719)
It's hard to rewrite after using indicator_eq_sum_single and prod_indicator_index, so I add these two lemmas.