Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-09-12 14:29
7407accc
View on Github →
chore: grind some proofs in the CHSH inequality (
#29333
)
Estimated changes
Modified
Mathlib/Algebra/Star/CHSH.lean
deleted
theorem
TsirelsonInequality.tsirelson_inequality_aux