Commit 2023-03-28 18:09 02c081e8

View on Github →

feat: port Algebra.Star.CHSH (#3135)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Star/Basic.lean

added theorem star_ofNat

Created Mathlib/Algebra/Star/CHSH.lean

added theorem CHSH_id

added theorem CHSH_inequality_of_comm

added structure IsCHSHTuple

added theorem TsirelsonInequality.sqrt_two_inv_mul_self

added theorem TsirelsonInequality.tsirelson_inequality_aux

added theorem tsirelson_inequality

Modified Mathlib/Data/Nat/Cast/Basic.lean

added theorem map_ofNat