OAI/Combinatorics/KMedianRecovery/Sampling/TensorEquiv.lean
6 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.MetricKMedianRecovery.BitMachine.BinarySeed.countline 7 - lemma
OAI.MetricKMedianRecovery.BitMachine.BinarySeed.count_eqline 10 - def
OAI.MetricKMedianRecovery.BitMachine.BinarySeed.tensorEquivline 14 - lemma
OAI.MetricKMedianRecovery.BitMachine.BinarySeed.tensorEquiv_consline 19 - lemma
OAI.MetricKMedianRecovery.BitMachine.BinarySeed.raw_tensorEquivline 21 - lemma
OAI.MetricKMedianRecovery.BitMachine.BinarySeed.nest_flatline 39