OAI/NumberTheory/SiegelZeros/LocalAlgebra/CoefficientSubspaceEquiv.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SiegelZeros.WeightedTorusJets.coefficientSubspaceEquiv line 16
  2. theorem OAI.SiegelZeros.WeightedTorusJets.coefficientSubspaceEquiv_apply line 35
  3. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_coefficient_subspace line 42
  4. theorem OAI.SiegelZeros.WeightedTorusJets.finrank_homogeneous_span line 54
  5. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_finset_homogeneous_span_eq_top line 73
  6. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_homogeneous_generic_basis line 98
  7. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.fraction_finrank_eq_pos line 135
  8. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_quotient_span_eq_zero_of_full_rank line 145
  9. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.generic_fiber_finrank_eq line 154
  10. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_common_degree_independent line 170
  11. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_gradedPiece_le_shifted_submodule line 206
  12. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.finrank_gradedSubmodule_le line 230
  13. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.exists_hilbert_finrank_sandwich line 239
  14. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.leadingCoeff_nonneg_of_eventually_nat_eval_nonneg line 288
  15. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.natDegree_leadingCoeff_eq_of_eventually_nat_eval_sandwich line 294
  16. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.natDegree_leadingCoeff_eq_of_eventually_binomial_sandwich line 347
  17. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.hilbertPolynomial_degree_coefficient_eq_rank line 408
  18. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.graded_quotient_coeLinearMap_injective line 448
  19. theorem OAI.SiegelZeros.WeightedTorusJets.Geometry.graded_quotient_coeLinearMap_surjective line 487
  20. def OAI.SiegelZeros.WeightedTorusJets.Geometry.gradedQuotientDecomposition line 502