OAI/NumberTheory/SiegelZeros/Selection/RowReplacement.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.W19.invariantDerivation_commute line 24
  2. def OAI.SiegelZeros.WeightedTorusJets.W19.iteratedInvariant line 35
  3. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iteratedInvariant_commute line 39
  4. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iteratedInvariant_monomial line 47
  5. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iteratedInvariant_zero line 59
  6. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iteratedInvariant_add line 67
  7. theorem OAI.SiegelZeros.WeightedTorusJets.W19.iteratedInvariant_smul line 75
  8. def OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant line 83
  9. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_zero line 88
  10. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_add line 92
  11. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_smul line 97
  12. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_sum line 102
  13. theorem OAI.SiegelZeros.WeightedTorusJets.W19.mixedInvariant_monomial line 110
  14. theorem OAI.SiegelZeros.WeightedTorusJets.W19.derivative_row_at_one line 117
  15. theorem OAI.SiegelZeros.WeightedTorusJets.W19.eigenvalue_map line 124
  16. theorem OAI.SiegelZeros.WeightedTorusJets.W19.derivative_row_endomorphisms line 129
  17. def OAI.SiegelZeros.WeightedTorusJets.W40.rowEntry line 149
  18. def OAI.SiegelZeros.WeightedTorusJets.W40.replacementCoefficient line 151
  19. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_expansion_second line 153
  20. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_expansion_third line 165
  21. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacementCoefficient_zero line 172
  22. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_leading_term line 176
  23. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_original_add_lower line 180
  24. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_vector_original_add_lower line 189
  25. theorem OAI.SiegelZeros.WeightedTorusJets.W40.shifted_first_index line 200
  26. def OAI.SiegelZeros.WeightedTorusJets.W40.weight line 207
  27. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_weight_lt_second line 209
  28. theorem OAI.SiegelZeros.WeightedTorusJets.W40.replacement_weight_lt_third line 217
  29. theorem OAI.SiegelZeros.WeightedTorusJets.W40.rowEntry_eq_actual_jet line 223