Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-13 09:36 e19473a9

View on Github →

feat(algebra/pointwise): Multiplying a singleton (#10660) and other lemmas about finset.product and singletons.

Estimated changes

Modified src/algebra/pointwise.lean

added theorem finset.mem_one

added theorem finset.mul_singleton

deleted theorem finset.mul_singleton_zero_subset

added theorem finset.mul_zero_subset

added theorem finset.nonempty.mul_zero

added theorem finset.nonempty.zero_mul

added theorem finset.one_subset

added theorem finset.singleton_mul

added theorem finset.singleton_mul_singleton

deleted theorem finset.singleton_zero_mul_subset

added theorem finset.zero_mul_subset

Modified src/data/finset/prod.lean

added theorem finset.product_singleton

added theorem finset.singleton_product

added theorem finset.singleton_product_singleton