OAI/NumberTheory/SiegelZeros/Selection/OrderedGreedyRows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SiegelZeros.WeightedTorusJets.W62.orderedSelected line 13
2. theorem OAI.SiegelZeros.WeightedTorusJets.W62.orderedSelected_mem line 17
3. theorem OAI.SiegelZeros.WeightedTorusJets.W62.orderedSelected_weight_le line 22
4. theorem OAI.SiegelZeros.WeightedTorusJets.W62.lower_weight_mem_cutoff line 27
5. theorem OAI.SiegelZeros.WeightedTorusJets.W62.lower_weight_ordered_span line 32
6. theorem OAI.SiegelZeros.WeightedTorusJets.W62.orderedSelected_det_of_spanning line 42
7. def OAI.SiegelZeros.WeightedTorusJets.W62.orderedCoords line 48
8. theorem OAI.SiegelZeros.WeightedTorusJets.W62.orderedCoords_injective line 52
9. theorem OAI.SiegelZeros.WeightedTorusJets.W62.orderedCoords_weight_le line 57