mathlib

dfca2b0f - feat(data/sym/sym2): add lemma that eq from distinct common members (#11563)

feat(data/sym/sym2): add lemma that eq from distinct common members (#11563) Two terms of type `sym2 a` are equal if one can find two distinct elements of type `a` that are members of both.