Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-21 18:29 eba78710

View on Github →

feat(data/finset/pointwise): |s| ∣ |s * t| (#18663)

Estimated changes

Modified src/data/finset/basic.lean

added theorem finset.forall_of_forall_cons

added theorem finset.forall_of_forall_insert

Modified src/data/finset/n_ary.lean

added theorem finset.card_dvd_card_image₂_left

added theorem finset.card_dvd_card_image₂_right

Modified src/data/finset/pointwise.lean

added theorem finset.card_dvd_card_mul_left

added theorem finset.card_dvd_card_smul_right