Commit 2025-11-29 02:24 6f417e45

View on Github →

feat(Data/Sym/Sym2): add Sym2.diagSet (#30559) Sym2.diagSet is the set of elements on the diagonal.

Estimated changes

Modified Mathlib/Data/Sym/Sym2.lean

deleted theorem Sym2.IsDiag.mem_range_diag

added def Sym2.diagSet

added theorem Sym2.diagSet_compl_eq_fromRel_ne

added theorem Sym2.diagSet_compl_eq_setOf_not_isDiag

added theorem Sym2.diagSet_eq_fromRel_eq

added theorem Sym2.diagSet_eq_setOf_isDiag

added theorem Sym2.diagSet_eq_univ_of_subsingleton

added theorem Sym2.irreflexive_iff_fromRel_subset_diagSet_compl

added theorem Sym2.isDiag_of_subsingleton

added theorem Sym2.mem_diagSet_iff_eq

added theorem Sym2.mem_diagSet_iff_isDiag

added theorem Sym2.reflexive_iff_diagSet_subset_fromRel