OAI/NumberTheory/SiegelZeros/Structure/InvariantJetLinearMap.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantJet_add_multiindex line 18
  2. def OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantJetLinearMap line 24
  3. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantJet_mem_span_monomials line 35
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.invariantJet_map line 53
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.eval_one_invariantJet_sum_monomials line 60
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.detects_jet_rows_of_polynomial_detection line 81
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.span_jet_rows_eq_top_of_polynomial_detection line 119
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.span_jet_rows_eq_top_of_polynomial_detection_over line 132
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.detects_jet_rows_of_polynomial_detection_set line 154
  10. theorem OAI.SiegelZeros.WeightedTorusJets.span_rows_eq_top_of_detects_set line 189
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.span_jet_rows_eq_top_of_polynomial_detection_set_over line 209
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.source_eigenvalue_row_eq_galois_row line 236
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.source_rectangle_span_of_polynomial_zero_test line 246
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.source_weighted_cutoff_span_of_polynomial_zero_test line 290
  15. def OAI.SiegelZeros.WeightedTorusJets.biquadraticDirections line 318
  16. def OAI.SiegelZeros.WeightedTorusJets.biquadraticCoefficients line 321
  17. def OAI.SiegelZeros.WeightedTorusJets.biquadraticForm line 324
  18. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticForm_apply line 327
  19. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticForm_ne_zero line 332
  20. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticForm_direction line 337
  21. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticDirections_linearIndependent line 341
  22. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_ker_biquadraticForm line 358
  23. theorem OAI.SiegelZeros.WeightedTorusJets.span_biquadraticDirections_eq_ker line 368
  24. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticCoefficients_linearIndependent line 380
  25. theorem OAI.SiegelZeros.WeightedTorusJets.mul_biquadraticCoefficients line 399
  26. theorem OAI.SiegelZeros.WeightedTorusJets.exists_basis_scaled_biquadraticCoefficients line 405
  27. theorem OAI.SiegelZeros.WeightedTorusJets.map_biquadraticCoefficients line 413
  28. theorem OAI.SiegelZeros.WeightedTorusJets.map_biquadraticDirections line 418
  29. theorem OAI.SiegelZeros.WeightedTorusJets.biquadraticCoefficients_linearIndependent_map line 424
  30. def OAI.SiegelZeros.WeightedTorusJets.biquadraticDirectionBasis line 432
  31. theorem OAI.SiegelZeros.WeightedTorusJets.coe_biquadraticDirectionBasis line 438
  32. theorem OAI.SiegelZeros.WeightedTorusJets.source_same_witness_hyperplane line 447
  33. theorem OAI.SiegelZeros.WeightedTorusJets.actual_biquadratic_rectangle_span line 471