Commit 2026-04-17 18:38 18c88f69

View on Github →

refactor(Pointwise/Finset): use IsLeftRegular/IsRightRegular (#38100) Use IsLeftRegular/IsRightRegular in card_le_card_mul_left_of_injective and card_le_card_mul_right_of_injective. Rename smul_finset_card_le to card_smul_finset_le with deprecation aliases.

Estimated changes

Modified Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean

modified theorem Finset.card_le_card_mul_left_of_injective

modified theorem Finset.card_le_card_mul_right_of_injective

Modified Mathlib/Algebra/Group/Pointwise/Finset/Scalar.lean

added theorem Finset.card_smul_finset_le

deleted theorem Finset.smul_finset_card_le