Braid relation/Yang-Baxter equation

Stream: Is there code for X?

[Brendan Seamas Murphy]

Has the yang baxter equation for braided monoidal categories been proven in mathlib? If not, are there any other instances of this relation in mathlib? I need it for something and if I have to prove it on my own I would like to be consistent with any prior naming conventions

[Johan Commelin]

I think it's not been done yet. But not 100% sure

[Adam Topaz]

I think @Scott Morrison is the person to ask.

[Brendan Seamas Murphy]

For reference here's the work I was doing involving it https://github.com/leanprover-community/mathlib4/compare/master...MonoidalOppositeStuff

[Kim Morrison]

I don't think it's been done.