Commit 2024-11-25 21:33 6e1b4171

View on Github →

chore(Pointwise): rename image_inv to image_inv_eq_inv (#19480) This is to make space for f '' s⁻¹ = (f '' s)⁻¹. Also rename smul_card_le to card_smul_le. From LeanCamCombi

Estimated changes

added theorem Finset.card_smul_le
modified theorem Finset.coe_inv
modified theorem Finset.image_inv
deleted theorem Finset.smul_card_le
modified theorem Set.image_inv
added theorem Set.image_inv_eq_inv
modified theorem Set.inv_singleton