OAI/NumberTheory/SiegelZeros/Structure/LinearVariableBasis.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.finite_normalization_local_finrank_eq_length_mul_rank line 21
  2. theorem OAI.SiegelZeros.WeightedTorusJets.GeometryAcceptance.mem_minimalPrimes_of_local_radical_eq_maximal line 43
  3. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.linearVariableBasis line 61
  4. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.linearVariableBasis_apply line 66
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.normalization_linearForms_independent line 70
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.symmetric_basis_coordinate_mem_degree_one line 89
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.symmetric_standard_coordinates line 105
  8. def OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis line 117
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_X line 123
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_symm_X_homogeneous line 128
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_homogeneous line 136
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_symm_homogeneous line 146
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.basis_sumExtend_inl line 156
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.exists_linearBasis_extension line 162
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.totalDegree_algHom_le_of_linear_images line 193
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_totalDegree line 206
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_symm_totalDegree line 222
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.exists_normalization_linear_coordinates line 230
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.exists_normalization_linear_coordinates_of_count line 259
  20. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.quotient_length_congr_ideal line 286
  21. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.quotient_finrank_congr_ideal line 292
  22. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_weighted_length_le_pow line 299
  23. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.DegreeBezout.linear_normalization_weighted_local_length_le line 346