OAI/NumberTheory/Jacobsthal/Siegel/InvariantJetLinearMap.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.invariantJet_add_multiindex line 20
  2. def OAI.Erdos970.WeightedTorusJets.Geometry.invariantJetLinearMap line 26
  3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.invariantJet_mem_span_monomials line 37
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.invariantJet_map line 55
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.eval_one_invariantJet_sum_monomials line 62
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.detects_jet_rows_of_polynomial_detection line 83
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.span_jet_rows_eq_top_of_polynomial_detection line 124
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.span_jet_rows_eq_top_of_polynomial_detection_over line 137
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.detects_jet_rows_of_polynomial_detection_set line 159
  10. theorem OAI.Erdos970.WeightedTorusJets.span_rows_eq_top_of_detects_set line 194
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.span_jet_rows_eq_top_of_polynomial_detection_set_over line 214
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.source_eigenvalue_row_eq_galois_row line 241
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.source_rectangle_span_of_polynomial_zero_test line 251
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.source_weighted_cutoff_span_of_polynomial_zero_test line 300
  15. def OAI.Erdos970.WeightedTorusJets.biquadraticDirections line 328
  16. def OAI.Erdos970.WeightedTorusJets.biquadraticCoefficients line 331
  17. def OAI.Erdos970.WeightedTorusJets.biquadraticForm line 334
  18. theorem OAI.Erdos970.WeightedTorusJets.biquadraticForm_apply line 337
  19. theorem OAI.Erdos970.WeightedTorusJets.biquadraticForm_ne_zero line 342
  20. theorem OAI.Erdos970.WeightedTorusJets.biquadraticForm_direction line 347
  21. theorem OAI.Erdos970.WeightedTorusJets.biquadraticDirections_linearIndependent line 351
  22. theorem OAI.Erdos970.WeightedTorusJets.finrank_ker_biquadraticForm line 368
  23. theorem OAI.Erdos970.WeightedTorusJets.span_biquadraticDirections_eq_ker line 378
  24. theorem OAI.Erdos970.WeightedTorusJets.biquadraticCoefficients_linearIndependent line 390
  25. theorem OAI.Erdos970.WeightedTorusJets.mul_biquadraticCoefficients line 409
  26. theorem OAI.Erdos970.WeightedTorusJets.exists_basis_scaled_biquadraticCoefficients line 415
  27. theorem OAI.Erdos970.WeightedTorusJets.map_biquadraticCoefficients line 423
  28. theorem OAI.Erdos970.WeightedTorusJets.map_biquadraticDirections line 428
  29. theorem OAI.Erdos970.WeightedTorusJets.biquadraticCoefficients_linearIndependent_map line 434
  30. def OAI.Erdos970.WeightedTorusJets.biquadraticDirectionBasis line 442
  31. theorem OAI.Erdos970.WeightedTorusJets.coe_biquadraticDirectionBasis line 448
  32. theorem OAI.Erdos970.WeightedTorusJets.source_same_witness_hyperplane line 457
  33. theorem OAI.Erdos970.WeightedTorusJets.actual_biquadratic_rectangle_span line 481