Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-04-03 02:27 7043a4ab

View on Github →

feat(algebra/pointwise): pointwise addition and multiplication of sets (#854)

Estimated changes

Created src/algebra/pointwise.lean

added theorem set.empty_pointwise_mul

added theorem set.mem_pointwise_mul

added theorem set.mem_pointwise_one

added theorem set.mul_mem_pointwise_mul

added def set.pointwise_add_add_monoid

added def set.pointwise_add_add_semigroup

added def set.pointwise_inv

added def set.pointwise_mul

added def set.pointwise_mul_comm_semiring

added theorem set.pointwise_mul_empty

added theorem set.pointwise_mul_eq_image

added def set.pointwise_mul_monoid

added def set.pointwise_mul_semigroup

added def set.pointwise_mul_semiring

added theorem set.pointwise_mul_subset_mul

added theorem set.pointwise_mul_union

added def set.pointwise_one

added def set.singleton.is_monoid_hom

added def set.singleton.is_mul_hom

added theorem set.union_pointwise_mul