OAI/Combinatorics/BalancedRyser/Candidates/CandidateConstituentTarget.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Balanced.CandidatePrescribed.constituentTargetCodesline 13 - theorem
OAI.Balanced.CandidatePrescribed.exposedLaw_apply_eq_zero_of_neline 17 - theorem
OAI.Balanced.CandidatePrescribed.expected_constituentTargetCodes_leline 24 - theorem
OAI.Balanced.CandidatePrescribed.expected_constituentTargetCodes_le_of_card_leline 62