Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-16 21:01 e186fbb7

View on Github →

feat(data/mv_polynomial): coeff_mul (#1216)

feat(data/mv_polynomial): coeff_mul
refactor(data/multiset): rename diagonal to antidiagonal
Rename diagonal to antidiagonal
Define antidiagonal as to_finsupp instead of to_finset
Add docstrings
fix build
Fix build

Estimated changes

Modified src/data/finsupp.lean

added def finsupp.antidiagonal

added theorem finsupp.antidiagonal_zero

added theorem finsupp.mem_antidiagonal_support

added theorem finsupp.swap_mem_antidiagonal_support

added theorem finsupp.to_multiset_to_finsupp

added def multiset.to_finsupp

added theorem multiset.to_finsupp_add

added theorem multiset.to_finsupp_apply

added theorem multiset.to_finsupp_singleton

added theorem multiset.to_finsupp_support

added theorem multiset.to_finsupp_to_multiset

added theorem multiset.to_finsupp_zero

Modified src/data/multiset.lean

added def multiset.antidiagonal

added theorem multiset.antidiagonal_coe'

added theorem multiset.antidiagonal_coe

added theorem multiset.antidiagonal_cons

added theorem multiset.antidiagonal_map_fst

added theorem multiset.antidiagonal_map_snd

added theorem multiset.antidiagonal_zero

added theorem multiset.card_antidiagonal

deleted theorem multiset.card_diagonal

deleted def multiset.diagonal

deleted theorem multiset.diagonal_coe'

deleted theorem multiset.diagonal_coe

deleted theorem multiset.diagonal_cons

deleted theorem multiset.diagonal_map_fst

deleted theorem multiset.diagonal_map_snd

deleted theorem multiset.diagonal_zero

added theorem multiset.mem_antidiagonal

deleted theorem multiset.mem_diagonal

modified theorem multiset.revzip_powerset_aux'

modified theorem multiset.revzip_powerset_aux

Modified src/data/mv_polynomial.lean

added theorem mv_polynomial.coeff_X'

modified theorem mv_polynomial.coeff_X

added theorem mv_polynomial.coeff_X_pow

added theorem mv_polynomial.coeff_mul

modified theorem mv_polynomial.coeff_mul_X'

modified theorem mv_polynomial.coeff_mul_X