Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-07-17 09:56 d6fd044c

View on Github →

feat(*): add nat.antidiagonal and use it for polynomial.mul_coeff (#1237)

Estimated changes

Modified src/data/finset.lean

added def finset.nat.antidiagonal

added theorem finset.nat.antidiagonal_zero

added theorem finset.nat.card_antidiagonal

added theorem finset.nat.mem_antidiagonal

Modified src/data/list/basic.lean

added def list.nat.antidiagonal

added theorem list.nat.antidiagonal_zero

added theorem list.nat.length_antidiagonal

added theorem list.nat.mem_antidiagonal

added theorem list.nat.nodup_antidiagonal

Modified src/data/multiset.lean

added def multiset.nat.antidiagonal

added theorem multiset.nat.antidiagonal_zero

added theorem multiset.nat.card_antidiagonal

added theorem multiset.nat.mem_antidiagonal

added theorem multiset.nat.nodup_antidiagonal

Modified src/data/polynomial.lean

added theorem polynomial.coeff_mul

deleted theorem polynomial.coeff_mul_left

deleted theorem polynomial.coeff_mul_right