Commit 2023-02-08 07:56 d22480f5

View on Github →

feat: port Data.Set.MulAntidiagonal (#2152)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Set/MulAntidiagonal.lean

added theorem Set.MulAntidiagonal.eq_of_fst_eq_fst

added theorem Set.MulAntidiagonal.eq_of_fst_le_fst_of_snd_le_snd

added theorem Set.MulAntidiagonal.eq_of_snd_eq_snd

added theorem Set.MulAntidiagonal.finite_of_isPwo

added theorem Set.MulAntidiagonal.finite_of_isWf

added theorem Set.MulAntidiagonal.fst_eq_fst_iff_snd_eq_snd

added theorem Set.mem_mulAntidiagonal

added def Set.mulAntidiagonal

added theorem Set.mulAntidiagonal_mono_left

added theorem Set.mulAntidiagonal_mono_right

added theorem Set.swap_mem_mulAntidiagonal

added theorem Set.swap_mem_mulAntidiagonal_aux