OAI/Combinatorics/KMedian/Projection/SeedCombinators.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedian.PCP.Compiler.SeedCombinators.sourceline 11 - lemma
OAI.MetricKMedian.PCP.Compiler.SeedCombinators.poly_sourceline 13 - def
OAI.MetricKMedian.PCP.Compiler.SeedCombinators.projectline 19 - lemma
OAI.MetricKMedian.PCP.Compiler.SeedCombinators.poly_projectline 23 - def
OAI.MetricKMedian.PCP.Compiler.SeedCombinators.numberedline 33 - lemma
OAI.MetricKMedian.PCP.Compiler.SeedCombinators.poly_numberedline 37