Commit 2023-01-16 08:55 ced2b4d5

View on Github →

feat: port Data.Multiset.Antidiagonal (#1562)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Multiset/Antidiagonal.lean

added def Multiset.antidiagonal

added theorem Multiset.antidiagonal_coe'

added theorem Multiset.antidiagonal_coe

added theorem Multiset.antidiagonal_cons

added theorem Multiset.antidiagonal_eq_map_powerset

added theorem Multiset.antidiagonal_map_fst

added theorem Multiset.antidiagonal_map_snd

added theorem Multiset.antidiagonal_zero

added theorem Multiset.card_antidiagonal

added theorem Multiset.mem_antidiagonal

added theorem Multiset.prod_map_add