Commit 2023-06-22 15:02 f68534cc

View on Github →

feat(data/finset/pointwise): |s| ∣ |s * t| (#5385) Forward-port leanprover-community/mathlib#18663 Also add a missing lemma.

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added theorem Finset.forall_of_forall_cons

added theorem Finset.forall_of_forall_insert

Modified Mathlib/Data/Finset/NAry.lean

added theorem Finset.card_dvd_card_image₂_left

added theorem Finset.card_dvd_card_image₂_right

Modified Mathlib/Data/Finset/Pointwise.lean

added theorem Finset.card_dvd_card_mul_left

added theorem Finset.card_dvd_card_mul_right

added theorem Finset.card_dvd_card_smul_right