Commit 2026-02-16 15:42 73ff1bf4

View on Github →

refactor(Data/Sym/Sym2): curry mk (#34803) Curry Sym2.mk from Sym2.mk (p : α × α) to Sym2.mk (a b : α). This matches the s(a, b) notation and reduce the uncertainty about simp normal form.

Estimated changes

modified def SimpleGraph.Dart.edge
modified theorem SimpleGraph.Dart.edge_mk
modified theorem Finset.sym2_eq_image
modified theorem Sym2.card_image_diag
modified theorem Sym2.card_image_offDiag
deleted theorem Set.mk'_mem_sym2_iff
modified theorem Set.mk_mem_sym2_iff
modified theorem Set.mk_preimage_sym2
modified theorem Set.sym2_eq_mk_image
modified theorem Set.sym2_image
deleted theorem Sym2.fromRel_proj_prop
deleted theorem Sym2.isDiag_iff_proj_eq
modified theorem Sym2.lift_mk
modified theorem Sym2.map_mk
deleted theorem Sym2.map_pair_eq
modified theorem Sym2.mk_eq_mk_iff
deleted theorem Sym2.mk_prod_swap_eq
modified theorem Sym2.mk_surjective
modified theorem Sym2.mul_mk
modified theorem Finsupp.sym2Mul_apply_mk