Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-17 12:38 07fb3d7e

View on Github →

refactor(data/finsupp/antidiagonal): Make antidiagonal a finset (#7595) Pursuant to discussion here Refactoring so that finsupp.antidiagonal and multiset.antidiagonal are finsets. ~~Still TO DO: multiset.antidiagonal~~

Estimated changes

Modified src/data/finsupp/antidiagonal.lean

added def finsupp.antidiagonal'

modified def finsupp.antidiagonal

added theorem finsupp.antidiagonal_filter_fst_eq

added theorem finsupp.antidiagonal_filter_snd_eq

deleted theorem finsupp.antidiagonal_support_filter_fst_eq

deleted theorem finsupp.antidiagonal_support_filter_snd_eq

modified theorem finsupp.antidiagonal_zero

added theorem finsupp.mem_antidiagonal

deleted theorem finsupp.mem_antidiagonal_support

deleted theorem finsupp.prod_antidiagonal_support_swap

added theorem finsupp.prod_antidiagonal_swap

added theorem finsupp.swap_mem_antidiagonal

deleted theorem finsupp.swap_mem_antidiagonal_support

Modified src/data/mv_polynomial/basic.lean

Modified src/data/mv_polynomial/variables.lean

Modified src/ring_theory/polynomial/homogeneous.lean

Modified src/ring_theory/power_series/basic.lean