OAI/Probability/FreeIsing/Spins/Twist.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Problem367.RootedBroadcast.measurePreserving_fairSpin_mulline 14 - theorem
OAI.Problem367.RootedBroadcast.measurePreserving_fairSpin_twistline 29 - theorem
OAI.Problem367.RootedBroadcast.map_pair_spinMul_of_indepFunline 40