Commit 2026-06-10 08:59 73b2611a

View on Github →

chore(Order/Defs/Unbundled): deprecate def Symmetric in favor of class Std.Symm (#38092)

Estimated changes

deleted theorem symmetric_isRelPrime
modified theorem CategoryTheory.Zag.symm
modified theorem CategoryTheory.Zigzag.symm
modified theorem SimpleGraph.isClique_pair
modified theorem Rel.card_interedges_comm
modified theorem Rel.edgeDensity_comm
modified theorem Rel.mk_mem_interedges_comm
modified theorem Rel.swap_mem_interedges_iff
modified theorem SimpleGraph.IsUniform.symm
modified theorem List.Pairwise.forall
modified theorem List.Pairwise.set_pairwise
modified theorem Multiset.Pairwise.forall
deleted theorem Nat.Coprime.symmetric
deleted theorem Computation.LiftRel.symm
added theorem Std.Symm.pairwise_on
deleted theorem Symmetric.pairwise_on
modified theorem pairwise_on_bool
modified def Set.sym2
modified theorem Sym2.diagSet_eq_fromRel_eq
modified theorem Sym2.diagSet_subset_fromRel
modified def Sym2.fromRel
modified def Sym2.fromRelOrderIso
modified theorem Sym2.fromRel_bot
modified theorem Sym2.fromRel_bot_iff
modified theorem Sym2.fromRel_irrefl
modified theorem Sym2.fromRel_mono_iff
modified theorem Sym2.fromRel_ne
modified theorem Sym2.fromRel_prop
modified theorem Sym2.fromRel_relationMap
modified theorem Sym2.fromRel_toRel
modified theorem Sym2.fromRel_top
modified theorem Sym2.fromRel_top_iff
modified theorem Sym2.toRel_fromRel
deleted theorem Sym2.toRel_symmetric
deleted theorem Stream'.WSeq.LiftRel.symm
modified theorem Relation.map_equivalence
deleted theorem Relation.map_symmetric
deleted theorem Relation.symmetric_join
added theorem Std.Symm.flip_eq
added theorem Std.Symm.swap_eq
deleted theorem Symmetric.comap
deleted theorem Symmetric.flip_eq
deleted theorem Symmetric.swap_eq
modified theorem flip_eq_iff
modified theorem swap_eq_iff
added theorem Equivalence.isEquiv
added theorem Equivalence.stdSymm
deleted theorem Equivalence.symmetric
deleted theorem symmetric_disjoint
modified theorem pairwise_iff_gt
modified theorem pairwise_iff_lt
modified theorem Specializes.symm