Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-01-26 15:54 ce2e7a85

View on Github →

feat(linear_algebra/multilinear): image of sum (#1908)

staging
fix build
linting
staging
docstring

Estimated changes

Modified src/algebra/big_operators.lean

added theorem finset.prod_piecewise

added theorem finset.prod_powerset_insert

Modified src/data/finset.lean

added theorem finset.empty_sdiff

added theorem finset.insert_sdiff_of_mem

added theorem finset.insert_sdiff_of_not_mem

modified theorem finset.lt_wf

added theorem finset.ne_insert_of_not_mem

added theorem finset.not_mem_of_mem_powerset_of_not_mem

added def finset.piecewise

added theorem finset.piecewise_coe

added theorem finset.piecewise_empty

added theorem finset.piecewise_eq_of_mem

added theorem finset.piecewise_eq_of_not_mem

added theorem finset.piecewise_insert

added theorem finset.piecewise_insert_of_ne

added theorem finset.piecewise_insert_self

added theorem finset.powerset_empty

added theorem finset.powerset_insert

Modified src/data/fintype.lean

added theorem finset.piecewise_univ

Modified src/data/set/basic.lean

deleted theorem set.insert_diff

added theorem set.insert_diff_of_mem

added theorem set.insert_diff_of_not_mem

added theorem set.ne_insert_of_not_mem

Modified src/data/set/function.lean

added theorem set.piecewise_empty

added theorem set.piecewise_eq_of_mem

added theorem set.piecewise_eq_of_not_mem

added theorem set.piecewise_insert

added theorem set.piecewise_insert_of_ne

added theorem set.piecewise_insert_self

added theorem set.piecewise_univ

Modified src/linear_algebra/multilinear.lean

added theorem multilinear_map.map_add_univ

added theorem multilinear_map.map_piecewise_add

added theorem multilinear_map.map_piecewise_smul

added theorem multilinear_map.map_smul_univ

added theorem multilinear_map.map_sub

Modified src/logic/function.lean

added def set.piecewise