OAI/NumberTheory/Jacobsthal/Siegel/LinearVariableBasis.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.finite_normalization_local_finrank_eq_length_mul_rank line 27
  2. theorem OAI.Erdos970.WeightedTorusJets.GeometryAcceptance.mem_minimalPrimes_of_local_radical_eq_maximal line 49
  3. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.linearVariableBasis line 68
  4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.linearVariableBasis_apply line 73
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.normalization_linearForms_independent line 77
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.symmetric_basis_coordinate_mem_degree_one line 96
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.symmetric_standard_coordinates line 112
  8. def OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis line 124
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_X line 130
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_symm_X_homogeneous line 135
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_homogeneous line 143
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_symm_homogeneous line 153
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.basis_sumExtend_inl line 163
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.exists_linearBasis_extension line 169
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.totalDegree_algHom_le_of_linear_images line 201
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_totalDegree line 214
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.polynomialCoordinatesOfLinearBasis_symm_totalDegree line 230
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.exists_normalization_linear_coordinates line 238
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.exists_normalization_linear_coordinates_of_count line 267
  20. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.quotient_length_congr_ideal line 294
  21. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.quotient_finrank_congr_ideal line 300
  22. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.coefficient_localization_weighted_length_le_pow line 307
  23. theorem OAI.Erdos970.WeightedTorusJets.Geometry.DegreeBezout.linear_normalization_weighted_local_length_le line 354