OAI/Combinatorics/EditApproximation/Queries/QueryGroupInputCost.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.EditApproximation.BinaryFraction.queryGroupInputsLengthline 9 - def
OAI.EditApproximation.BinaryFraction.queryGroupInputsBitBudgetline 12 - theorem
OAI.EditApproximation.BinaryFraction.queryGroupInputsWithWork_boundsline 18