Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-23 19:55 cce4e962

View on Github →

feat(data/finset/pointwise): allow lifting monoid homs to finsets (#16935)

Estimated changes

Modified src/data/finset/pointwise.lean

modified theorem finset.image_div

added def finset.image_monoid_hom

modified theorem finset.image_mul

added def finset.image_mul_hom

added def finset.image_one_hom