OAI/NumberTheory/PiExponent/Polynomials/HomogeneousHilbertExistence.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.PiExponentJets.W64.iteratedColon_eq_colon_powerline 15 - theorem
OAI.PiExponentJets.W64.sectionHilbertSeries_renameline 22 - theorem
OAI.PiExponentJets.W64.sectionHilbertSeries_coordinateline 30 - theorem
OAI.PiExponentJets.W64.exists_homogeneous_hilbert_numeratorline 38