mathlib3

8289518d - feat(algebra/star): the Bell/CHSH/Tsirelson inequalities (#4687)

feat(algebra/star): the Bell/CHSH/Tsirelson inequalities (#4687) Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>