Commit 2023-12-30 05:21 d54b614b

View on Github →

feat(*/Pointwise): generalize some lemmas to SMulZeroClass (#9243)

Estimated changes

Modified Mathlib/Data/Finset/Pointwise.lean

modified theorem Finset.Nonempty.smul_zero

modified theorem Finset.smul_zero_subset

modified theorem Finset.zero_mem_smul_finset

modified theorem Finset.zero_mem_smul_finset_iff

Modified Mathlib/Data/Set/Pointwise/SMul.lean

modified theorem Set.zero_mem_smul_set