Commit 2025-06-18 19:19 392e014a

feat(Pointwise): cardinality of product set in GroupWithZero (#24578) This PR:

• generalises the assumptions to card_le_card_image₂_left and card_le_card_image₂_right and golf these: they previously required injectivity everywhere despite using it in only one place. (These lemmas were also used in exactly one place each in mathlib)
• adds card_le_card_mul_left_of_injective and card_le_card_mul_right_of_injective which generalise the typeclass assumptions on the existing card_le_card_mul_left and card_le_card_mul_right
• uses the above to add versions of card_le_card_mul_left and card_le_card_mul_right in groups with zero. This is useful for applying the pointwise constructions to fields In fact, the first versions of all the above lemmas were written in this generality, but that was seemingly lost during an upstream.