OAI/Combinatorics/BalancedRyser/Probability/IndependentTrialGrouping.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.IndependentTrials.past_independent_currentline 14 - theorem
OAI.Balanced.IndependentTrials.pastCurrent_independent_futureline 20 - theorem
OAI.Balanced.IndependentTrials.independent_past_currentline 41 - theorem
OAI.Balanced.IndependentTrials.independent_past_current_futureline 46