TODO: Interface in Sym

Stream: mathlib4

[metakuntyyy]

The documentation mentions that this needs a fleshed out interface. https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Sym/Basic.html. What is meant by that and what theorems are needed.

I'm using Sym in my proof and I think there could be additional helpful definitions that could be added, but I'm also interested in working on this todo.

[Jakub Nowak]

This comment was there from the beginning mathlib3#3264. @Kyle Miller can maybe answer?