Commit 2023-02-11 08:36 24c35753

View on Github →

feat: Port Data.Finset.MulAntidiagonal (#2158)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/MulAntidiagonal.lean

added theorem Finset.isPwo_support_mulAntidiagonal

added theorem Finset.mem_mulAntidiagonal

added theorem Finset.mulAntidiagonal_min_mul_min

added theorem Finset.mulAntidiagonal_mono_left

added theorem Finset.mulAntidiagonal_mono_right

added theorem Finset.support_mulAntidiagonal_subset_mul

added theorem Finset.swap_mem_mulAntidiagonal

added theorem Set.IsPwo.mul

added theorem Set.IsWf.min_mul

added theorem Set.IsWf.mul