Mathlib Changelog
v4
Changelog
About
Github
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