Commit 2024-10-22 21:02 d50b9137

View on Github →

chore(Data): use newly introduced finset notation (#18059) 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 DFinsupp.support_filter
modified theorem DFinsupp.card_Icc
modified theorem DFinsupp.card_Ico
modified theorem DFinsupp.card_Iic
modified theorem DFinsupp.card_Iio
modified theorem DFinsupp.card_Ioc
modified theorem DFinsupp.card_Ioo
modified theorem DFinsupp.card_pi
modified theorem DFinsupp.card_uIcc
modified theorem Finset.card_dfinsupp
modified theorem Finset.card_finsupp
modified theorem Finsupp.card_pi
modified theorem Finset.mem_slice
modified def Finset.slice
modified theorem Finset.sum_card_slice
modified def Set.Sized
modified theorem Set.sized_singleton
modified theorem Finset.card_compls
modified theorem Finset.card_diffs_iff
modified theorem Finset.card_diffs_le
modified theorem Finset.card_disjSups_le
modified theorem Finset.card_infs_iff
modified theorem Finset.card_infs_le
modified theorem Finset.card_sups_iff
modified theorem Finset.card_sups_le
modified def Finset.disjSups
modified theorem Finsupp.support_filter
modified theorem Finsupp.card_Icc
modified theorem Finsupp.card_Ico
modified theorem Finsupp.card_Iic
modified theorem Finsupp.card_Iio
modified theorem Finsupp.card_Ioc
modified theorem Finsupp.card_Ioo
modified theorem Finset.card_compl
modified theorem Finset.card_eq_iff_eq_univ
modified theorem Finset.card_eq_of_equiv
modified theorem Finset.card_eq_of_equiv_fin
modified theorem Finset.card_fin
modified theorem Finset.card_le_univ
modified theorem Finset.card_univ
modified theorem Finset.eq_univ_of_card
modified theorem Fintype.card_coe
modified theorem card_finset_fin_le
modified theorem card_perms_of_finset
modified def finSumEquivOfFinset
modified theorem finSumEquivOfFinset_inl
modified theorem finSumEquivOfFinset_inr
modified theorem Int.Ico_filter_dvd_card
modified theorem Int.Ico_filter_dvd_eq
modified theorem Int.Ico_filter_modEq_card
modified theorem Int.Ico_filter_modEq_eq
modified theorem Int.Ioc_filter_dvd_card
modified theorem Int.Ioc_filter_dvd_eq
modified theorem Int.Ioc_filter_modEq_card
modified theorem Int.Ioc_filter_modEq_eq
modified theorem Nat.Ico_filter_modEq_card
modified theorem Nat.Ico_filter_modEq_cast
modified theorem Nat.Ioc_filter_modEq_card
modified theorem Nat.Ioc_filter_modEq_cast
modified theorem Int.card_Icc
modified theorem Int.card_Icc_of_le
modified theorem Int.card_Ico
modified theorem Int.card_Ico_of_le
modified theorem Int.card_Ioc
modified theorem Int.card_Ioc_of_le
modified theorem Int.card_Ioo
modified theorem Int.card_Ioo_of_lt
modified theorem Int.card_uIcc
modified theorem Nat.count_le_card
modified theorem Nat.count_lt_card
modified theorem Nat.card_multiples'
modified theorem Nat.card_multiples
modified theorem Nat.count_nth
modified theorem Nat.count_nth_succ
modified theorem Nat.image_nth_Iio_card
modified theorem Nat.isLeast_nth
modified theorem Nat.isLeast_nth_of_lt_card
modified theorem Nat.le_nth
modified theorem Nat.nth_eq_orderEmbOfFin
modified theorem Nat.nth_injOn
modified theorem Nat.nth_le_nth'
modified theorem Nat.nth_lt_nth'
modified theorem Nat.nth_mem
modified theorem Nat.nth_mem_of_lt_card
modified theorem Nat.nth_of_card_le
modified theorem Nat.sum_totient'
modified def Nat.totient
modified theorem Nat.totient_eq_card_coprime
modified theorem PNat.card_Icc
modified theorem PNat.card_Ico
modified theorem PNat.card_Ioc
modified theorem PNat.card_Ioo
modified theorem PNat.card_uIcc
modified theorem Pi.card_Icc
modified theorem Pi.card_Ici
modified theorem Pi.card_Ico
modified theorem Pi.card_Iic
modified theorem Pi.card_Iio
modified theorem Pi.card_Ioc
modified theorem Pi.card_Ioi
modified theorem Pi.card_Ioo
modified theorem Pi.card_uIcc
modified theorem Sigma.card_Icc
modified theorem Sigma.card_Ico
modified theorem Sigma.card_Ioc
modified theorem Sigma.card_Ioo
modified theorem Sym2.card_image_diag
modified theorem Sym2.card_image_offDiag