Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.subset_mul

Modification history

2022-05-02 21:37
src/data/finset/pointwise.lean
feat(data/finset/n_ary): Binary image of finsets (#13718) …
Modified finset.subset_mulView on Github →
2022-03-21 11:08
src/data/finset/pointwise.lean
split(data/{finset,set}/pointwise): Split off `algebra.pointwise` (#12831) …
Modified finset.subset_mulView on Github →
2021-01-27 18:19
src/algebra/pointwise.lean
feat(algebra/*,linear_algebra/basic,ring_theory/ideal): lemmas about span of finite subsets and nontrivial maximal ideals (#5641)
Added finset.subset_mulView on Github →