OAI/Combinatorics/KMedian/Machines/UnaryPolynomial.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.MetricKMedian.PCP.Compiler.unitList_eq_lengthline 12 - def
OAI.MetricKMedian.PCP.Compiler.unaryPowerline 14 - lemma
OAI.MetricKMedian.PCP.Compiler.unaryPower_lengthline 17 - lemma
OAI.MetricKMedian.PCP.Compiler.poly_unaryPowerline 22 - lemma
OAI.MetricKMedian.PCP.Compiler.poly_unaryPolynomialline 27