Commit 2024-10-22 12:48 90daa70a

View on Github →

chore(Algebra): use newly introduced finset notation (#18053) For s : Finset α, replace s.card with #s, s.filter p with {x ∈ s | p x}, ∑ x ∈ s.filter p, f x with ∑ x ∈ s with p x, f x. Rewrap lines around and open the Finset locale where necessary.

Estimated changes

modified theorem Finset.card_smul_expect
modified theorem Finset.card_eq_sum_ones
modified theorem Finset.card_filter
modified theorem Finset.pow_card_mul_prod
modified theorem Finset.prod_const
modified theorem Finset.prod_eq_pow_card
modified theorem Finset.prod_image'
modified theorem Finset.prod_mul_pow_card
modified theorem Finset.sum_const_nat
modified theorem UniqueMul.of_card_le_one
modified theorem uniqueMul_of_twoUniqueMul
modified theorem Finset.cast_card
modified theorem Finset.le_sum_card
modified theorem Finset.le_sum_card_inter
modified theorem Finset.sum_card
modified theorem Finset.sum_card_inter
modified theorem Finset.sum_card_inter_le
modified theorem Finset.sum_card_le
modified theorem sq_sum_le_card_mul_sum_sq