OAI/NumberTheory/Jacobsthal/Siegel/FinrankDegreePiecePosPrimeVariableNotMem.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.finrank_degreePiece_pos_of_prime_variable_not_mem line 22
2. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.hilbertPolynomial_ne_zero_of_prime_variable_not_mem line 32
3. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.projectiveDegree_pos_of_prime_variable_not_mem line 44
4. theorem OAI.Erdos970.WeightedTorusJets.Geometry.GradedQuotient.cone_projectiveDegree_pos line 56