Commit 2024-10-23 02:43 1eba96a6

View on Github →

chore: use newly introduced finset notation (#17974) 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 def SSet.horn.edge
modified theorem Equiv.Perm.IsCycle.isConj
modified theorem Equiv.Perm.IsCycle.sign
modified def Equiv.Perm.support
modified def hammingDist
modified def hammingNorm
modified def Affine.Simplex.face
modified theorem Lagrange.degree_nodal
modified theorem Lagrange.eq_interpolate
modified theorem Lagrange.natDegree_nodal
modified def Nat.divisors
modified theorem Nat.filter_dvd_eq_divisors
modified def Nat.properDivisors
modified theorem ZMod.gauss_lemma_aux
modified def primorial
modified theorem Finset.Ico_filter_le
modified theorem Finset.Ico_filter_lt
modified theorem Finset.Ioo_filter_lt
modified theorem Finset.filter_ge_eq_Iic
modified theorem Finset.filter_gt_eq_Iio
modified theorem Finset.filter_le_eq_Ici
modified theorem Finset.filter_lt_eq_Ioi
modified theorem Int.card_box
modified theorem Finset.card_Icc_prod
modified theorem Finset.card_Ici_prod
modified theorem Finset.card_Iic_prod
modified theorem Finset.card_uIcc_prod
modified theorem Fin.card_Icc
modified theorem Fin.card_Ici
modified theorem Fin.card_Ico
modified theorem Fin.card_Iic
modified theorem Fin.card_Iio
modified theorem Fin.card_Ioc
modified theorem Fin.card_Ioi
modified theorem Fin.card_Ioo
modified theorem Fin.card_uIcc
modified theorem Nat.card_Icc
modified theorem Nat.card_Ico
modified theorem Nat.card_Iic
modified theorem Nat.card_Iio
modified theorem Nat.card_Ioc
modified theorem Nat.card_Ioo
modified theorem Nat.card_uIcc
modified theorem Finpartition.card_bot
modified theorem Finpartition.card_mono
modified theorem Finpartition.sum_card_parts
modified theorem Finset.prod_X_add_C_coeff