Commit 2025-03-29 18:40 2fd59986

View on Github →

chore(*): use #s notation here and there (#23438)

Estimated changes

modified theorem Finset.card_inv
modified theorem Finset.card_inv_le
modified theorem Finset.card_le_card_pow
modified theorem Finset.card_mul_le
modified theorem Finset.card_mul_singleton
modified theorem Finset.card_one
modified theorem Finset.card_pow_le
modified theorem Finset.card_pow_mono
modified theorem Finset.card_singleton_mul
modified theorem Finset.div_card_le
modified theorem Finset.smul_finset_card_le
modified theorem Finset.vsub_card_le
modified theorem Equiv.Perm.sum_cycleType
modified theorem card_support_eq_three_iff