Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-09 09:29 5329bf3a

View on Github →

feat(algebra/pointwise): More lemmas on pointwise multiplication (#997)

feat(algebra/pointwise): More lemmas on pointwise multiplication
Fix build, hopefully
Fix build
to_additive + fix formatting

Estimated changes

Modified src/algebra/pointwise.lean

added theorem set.mem_smul_set

added theorem set.mul_subset_mul

added def set.pointwise_add_fintype

added def set.pointwise_mul_action

added def set.pointwise_mul_fintype

added def set.pointwise_mul_image_is_semiring_hom

added theorem set.smul_set_eq_image