Main results

The main results that the formalization.yaml of FormalFrontier/graded-rings lists under status.main_results at commit 6a459e8e, each that the scan finds declared in the file the yaml gives, with its line. They are listed here, not made articles: in several Formal Frontier libraries this list is close to the whole API. The notes are the yaml's.

Declaration Kind Where Note
Ideal.Quotient.gradedRing def GradedRings/Quotient.lean, line 191
GradedLocalization.gradedRing def GradedRings/Localization.lean, line 333
HomogeneousLocalization.mapDegreeMul def GradedRings/HomogeneousLocalizationMap.lean, line 78
GradedAlgebra.irrelevant_fg_iff_finiteType theorem GradedRings/FiniteType.lean, line 187
GradedAlgebra.isNoetherianRing_iff_gradeZero_and_irrelevant_fg theorem GradedRings/Noetherian.lean, line 46
Submodule.eq_iSup_pow_smul_span_singleton_of_isPrecomplete theorem GradedRings/FilteredModule/WeightedSpan.lean, line 231
Submodule.exists_eq_smul_of_weighted_generation theorem GradedRings/FilteredModule/Finiteness.lean, line 70
Submodule.moduleFinite_of_weighted_generation theorem GradedRings/FilteredModule/Finiteness.lean, line 100
Submodule.fg_of_weighted_generation theorem GradedRings/FilteredModule/Finiteness.lean, line 125
GradedRing.homogeneousPrimeEquivDegreeZeroPrime def GradedRings/HomogeneousPrime.lean, line 248
SymmetricAlgebra.gradedAlgebra instance GradedRings/SymmetricAlgebra.lean, line 61
PrimeMultiplicity.localizationValuation def GradedRings/PrimeMultiplicity.lean, line 136
HomogeneousLocalization.awayPrimeMultiplicityValuation def GradedRings/HomogeneousPrimeMultiplicity.lean, line 35
MvPolynomial.irreducible_of_awayPrimeMultiplicityValuation_eq_exp_one theorem GradedRings/MvPolynomialAway.lean, line 224
GradedRing.Veronese.VeroneseRing abbrev GradedRings/Veronese.lean, line 33
GradedRing.Veronese.inclusion def GradedRings/Veronese.lean, line 45
GradedRing.Veronese.inclusion_injective theorem GradedRings/Veronese.lean, line 185
GradedRing.Veronese.zeroRingEquiv def GradedRings/Veronese.lean, line 208
GradedRingHom.surjective_gradedAddHom theorem GradedRings/HomogeneousLifts.lean, line 30
MvPolynomial.isHomogeneous_aeval_degreeOne theorem GradedRings/HomogeneousLifts.lean, line 73
MvPolynomial.aevalDegreeOneGradedHom def GradedRings/HomogeneousLifts.lean, line 86
MvPolynomial.exists_isHomogeneous_aeval theorem GradedRings/HomogeneousLifts.lean, line 94
GradedRing.Veronese.adjoin_component_one_eq_top theorem GradedRings/VeroneseDegreeOne.lean, line 82
GradedRing.Veronese.CoherentTail.TailEquiv structure GradedRings/CoherentTailVeronese.lean, line 34
GradedRing.Veronese.CoherentTail.TailEquiv.selectedRingEquiv def GradedRings/CoherentTailVeronese.lean, line 229
GradedRing.Veronese.CoherentTail.TailEquiv.selectedGradedHom def GradedRings/CoherentTailVeronese.lean, line 250
GradedRing.Veronese.CoherentTail.TailEquiv.selectedGradedHomSymm_comp theorem GradedRings/CoherentTailVeronese.lean, line 265
GradedRing.Veronese.CoherentTail.TailEquiv.selectedGradedHom_comp_symm theorem GradedRings/CoherentTailVeronese.lean, line 273
GradedRing.Veronese.CoherentTail.TailEquiv.selected_zero theorem GradedRings/CoherentTailVeronese.lean, line 282
Finsupp.weightedBlockSize def GradedRings/WeightedBlocks.lean, line 25
Finsupp.weightedBlockSize_pos theorem GradedRings/WeightedBlocks.lean, line 28
Finsupp.exists_weightedBlocks theorem GradedRings/WeightedBlocks.lean, line 126
MvPolynomial.IsWeightedHomogeneous.aeval_mem theorem GradedRings/WeightedEvaluation.lean, line 40
MvPolynomial.weightedAevalGradedHom def GradedRings/WeightedEvaluation.lean, line 51
MvPolynomial.aeval_weightedHomogeneousComponent theorem GradedRings/WeightedEvaluation.lean, line 59
MvPolynomial.exists_isWeightedHomogeneous_aeval theorem GradedRings/WeightedEvaluation.lean, line 74
MvPolynomial.IsWeightedHomogeneous.mem_adjoin_weightedBlockSize theorem GradedRings/WeightedBlockAdjoin.lean, line 47
GradedRing.Veronese.exists_finite_degree_one_generators theorem GradedRings/FiniteVeronese.lean, line 33
GradedRing.Veronese.exists_positive_finite_degree_one_generators theorem GradedRings/FiniteVeronese.lean, line 116
MvPolynomial.exists_finset_weightedVeronese_generators theorem GradedRings/WeightedVeroneseGenerators.lean, line 131
GradedRing.Veronese.finiteType_of_finite_homogeneous_generators theorem GradedRings/VeroneseFiniteType.lean, line 38
GradedRing.Veronese.finiteType_of_finiteType theorem GradedRings/VeroneseFiniteType.lean, line 107
GradedRing.Veronese.zeroRingEquivAll def GradedRings/VeroneseZero.lean, line 38
GradedRing.Veronese.of_zero_eq_algebraMap_mul_pow theorem GradedRings/VeroneseZero.lean, line 118
GradedRing.Veronese.aeval_zeroVariable_surjective theorem GradedRings/VeroneseZero.lean, line 155
GradedRing.Veronese.finiteType_zero theorem GradedRings/VeroneseZero.lean, line 173
GradedRing.Veronese.inclusion_finite theorem GradedRings/VeroneseFinite.lean, line 34
GradedRing.Veronese.residueProjection def GradedRings/VeroneseResidue.lean, line 117
GradedRing.Veronese.residueProjection_of_mem theorem GradedRings/VeroneseResidue.lean, line 140
GradedRing.Veronese.residueProjection_idempotent theorem GradedRings/VeroneseResidue.lean, line 134
GradedRing.Veronese.mem_residueProjection_range_iff theorem GradedRings/VeroneseResidue.lean, line 146
GradedRing.Veronese.residueProjection_range_finite theorem GradedRings/VeroneseResidue.lean, line 160
GradedRing.Veronese.residueProjection_range_finite_of_finiteType theorem GradedRings/VeroneseResidue.lean, line 170
GradedRing.Veronese.ResidueModule abbrev GradedRings/VeroneseResidueModule.lean, line 36
GradedRing.Veronese.instResidueModule instance GradedRings/VeroneseResidueModule.lean, line 47
GradedRing.Veronese.residueEvaluation def GradedRings/VeroneseResidueModule.lean, line 66
GradedRing.Veronese.residueEvaluation_injective theorem GradedRings/VeroneseResidueModule.lean, line 115
GradedRing.Veronese.residueEvaluation_range_eq theorem GradedRings/VeroneseResidueModule.lean, line 164
GradedRing.Veronese.residueEvaluationEquiv def GradedRings/VeroneseResidueModule.lean, line 200
GradedRing.Veronese.residueModule_finite theorem GradedRings/VeroneseResidueModule.lean, line 218
GradedRing.Veronese.residueModule_finite_of_finiteType theorem GradedRings/VeroneseResidueModule.lean, line 229

Quoted from the main results in formalization.yaml of FormalFrontier/graded-rings at commit 6a459e8e, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.