OAI/Combinatorics/BalancedRyser/Deletion/UniformDeletionMoments.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Balanced.UniformDeletion.eval_eq_iff_joining_directionline 13 - theorem
OAI.Balanced.UniformDeletion.card_forbidden_pairline 26 - theorem
OAI.Balanced.UniformDeletion.pair_survivalline 39 - theorem
OAI.Balanced.UniformDeletion.expected_core_sq_sumline 67 - theorem
OAI.Balanced.UniformDeletion.expected_core_sqline 91