Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-11-25 01:40
d04f5a55
View on Github →
feat(algebra/pointwise): lemmas about multiplication of finsets (
#10455
)
Estimated changes
Modified
src/algebra/pointwise.lean
modified
theorem
finset.coe_mul
added
theorem
finset.empty_mul
modified
theorem
finset.mem_mul
modified
theorem
finset.mul_card_le
modified
theorem
finset.mul_def
added
theorem
finset.mul_empty
modified
theorem
finset.mul_mem_mul
added
theorem
finset.mul_nonempty_iff
added
theorem
finset.mul_singleton_zero
added
theorem
finset.mul_subset_mul
added
theorem
finset.singleton_zero_mul