OAI/NumberTheory/Jacobsthal/Siegel/CoefficientSubspaceEquiv.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.WeightedTorusJets.coefficientSubspaceEquiv line 19
  2. theorem OAI.Erdos970.WeightedTorusJets.coefficientSubspaceEquiv_apply line 38
  3. theorem OAI.Erdos970.WeightedTorusJets.finrank_coefficient_subspace line 45
  4. theorem OAI.Erdos970.WeightedTorusJets.finrank_homogeneous_span line 57
  5. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_finset_homogeneous_span_eq_top line 76
  6. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_homogeneous_generic_basis line 101
  7. theorem OAI.Erdos970.WeightedTorusJets.Geometry.fraction_finrank_eq_pos line 138
  8. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_quotient_span_eq_zero_of_full_rank line 148
  9. theorem OAI.Erdos970.WeightedTorusJets.Geometry.generic_fiber_finrank_eq line 157
  10. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_common_degree_independent line 173
  11. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_gradedPiece_le_shifted_submodule line 209
  12. theorem OAI.Erdos970.WeightedTorusJets.Geometry.finrank_gradedSubmodule_le line 233
  13. theorem OAI.Erdos970.WeightedTorusJets.Geometry.exists_hilbert_finrank_sandwich line 242
  14. theorem OAI.Erdos970.WeightedTorusJets.Geometry.leadingCoeff_nonneg_of_eventually_nat_eval_nonneg line 292
  15. theorem OAI.Erdos970.WeightedTorusJets.Geometry.natDegree_leadingCoeff_eq_of_eventually_nat_eval_sandwich line 298
  16. theorem OAI.Erdos970.WeightedTorusJets.Geometry.natDegree_leadingCoeff_eq_of_eventually_binomial_sandwich line 351
  17. theorem OAI.Erdos970.WeightedTorusJets.Geometry.hilbertPolynomial_degree_coefficient_eq_rank line 414
  18. theorem OAI.Erdos970.WeightedTorusJets.Geometry.graded_quotient_coeLinearMap_injective line 456
  19. theorem OAI.Erdos970.WeightedTorusJets.Geometry.graded_quotient_coeLinearMap_surjective line 495
  20. def OAI.Erdos970.WeightedTorusJets.Geometry.gradedQuotientDecomposition line 510