Main results

The main results that the formalization.yaml of FormalFrontier/multivariate-polynomials lists under status.main_results at commit 724d9804, 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
Normal.orbit_eq_rootSet_minpoly	theorem	MultivariatePolynomials/PolynomialRootOrbits.lean, line 39
Normal.ncard_orbit_eq_natSepDegree	theorem	MultivariatePolynomials/PolynomialRootOrbits.lean, line 49
Normal.ncard_orbit_eq_natDegree_iff_isSeparable	theorem	MultivariatePolynomials/PolynomialRootOrbits.lean, line 58
MaximalSpectrum.infinite_polynomial	theorem	MultivariatePolynomials/PrimeSpectrum.lean, line 190
MaximalSpectrum.infinite_mvPolynomial_iff	theorem	MultivariatePolynomials/PrimeSpectrum.lean, line 202
MvPolynomial.exists_finset_fractionRing_map_range	theorem	MultivariatePolynomials/FractionRingFiniteVariables.lean, line 51
MvPolynomial.ideal_span_X_sub_C_eq_ker_eval	theorem	MultivariatePolynomials/EvaluationIdeal.lean, line 222
MvPolynomial.mem_ideal_span_X_sub_C_iff	theorem	MultivariatePolynomials/EvaluationIdeal.lean, line 249
MvPolynomial.ideal_span_X_sub_C_eq_vanishingIdeal_singleton	theorem	MultivariatePolynomials/EvaluationIdeal.lean, line 348
MvPolynomial.pointSquareZeroForward	def	MultivariatePolynomials/PointSquareZeroPresentation.lean, line 230
MvPolynomial.pointSquareZeroForward_bijective	theorem	MultivariatePolynomials/PointSquareZeroQuotient.lean, line 125
MvPolynomial.pointSquareZeroAlgEquiv	def	MultivariatePolynomials/PointSquareZeroQuotient.lean, line 216
MvPolynomial.idealOfVars_not_fg	theorem	MultivariatePolynomials/IdealOfVars.lean, line 162
MvPolynomial.IsWeightedHomogeneous.eval₂Hom_scaleVariables	theorem	MultivariatePolynomials/HomogeneousEvaluation.lean, line 34
MvPolynomial.IsHomogeneous.eval₂Hom_mul_left	theorem	MultivariatePolynomials/HomogeneousEvaluation.lean, line 67
MvPolynomial.blockSubst	def	MultivariatePolynomials/BlockSubstitution.lean, line 33
MvPolynomial.eval_blockSubst	theorem	MultivariatePolynomials/BlockSubstitution.lean, line 38
MvPolynomial.eval_blockSubst_eq_zero_imp	theorem	MultivariatePolynomials/BlockSubstitution.lean, line 47
MvPolynomial.eval_blockSubst_eq_zero_iff	theorem	MultivariatePolynomials/BlockSubstitution.lean, line 60
MvPolynomial.ne_zero_of_eval_eq_zero_imp	theorem	MultivariatePolynomials/BlockSubstitution.lean, line 79
MvPolynomial.iteratedBlockSubst	def	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 40
MvPolynomial.iteratedBlockSubst_zero	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 47
MvPolynomial.iteratedBlockSubst_succ	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 50
MvPolynomial.eval_iteratedBlockSubst_zero	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 57
MvPolynomial.eval_iteratedBlockSubst_succ	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 61
MvPolynomial.eval_iteratedBlockSubst_eq_zero_imp	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 69
MvPolynomial.eval_iteratedBlockSubst_eq_zero_iff	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 89
MvPolynomial.isHomogeneous_iteratedBlockSubst	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 112
MvPolynomial.iteratedBlockSubst_ne_zero	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 131
MvPolynomial.iteratedBlockSubst_totalDegree	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 137
MvPolynomial.exists_iteratedBlockSubst_totalDegree_gt	theorem	MultivariatePolynomials/IteratedBlockSubstitution.lean, line 145
MvPolynomial.rename_blockSubst	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 38
MvPolynomial.blockSubst_assoc	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 47
MvPolynomial.blockSubst_X_left	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 60
MvPolynomial.blockSubst_X_right	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 65
MvPolynomial.iteratedBlockSubst_one	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 138
MvPolynomial.iteratedBlockSubst_add	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 184
MvPolynomial.iteratedBlockSubst_snoc	theorem	MultivariatePolynomials/BlockSubstitutionLaws.lean, line 211
MvPolynomial.totalDegree_blockSubst	theorem	MultivariatePolynomials/BlockSubstitutionDegree.lean, line 308
MvPolynomial.IsHomogeneous.coeff_polynomial_interchange	theorem	MultivariatePolynomials/PolynomialCoefficientHomogeneity.lean, line 108
MvPolynomial.eval_addMonoidAlgebraMap_of_linearMap	theorem	MultivariatePolynomials/LinearCoefficientEvaluation.lean, line 38
MonomialOrder.linearDivisionQuotient	def	MultivariatePolynomials/LinearDivision.lean, line 66
MonomialOrder.linearDivisionRemainder	def	MultivariatePolynomials/LinearDivision.lean, line 73
MonomialOrder.linearDivision_decomposition	theorem	MultivariatePolynomials/LinearDivision.lean, line 96
MonomialOrder.linearDivision_remainder_support	theorem	MultivariatePolynomials/LinearDivision.lean, line 152
MonomialOrder.linearMap_preserves_coeffsIn	theorem	MultivariatePolynomials/LinearDivision.lean, line 168
MonomialOrder.linearDivision_remainder_coeffsIn	theorem	MultivariatePolynomials/LinearDivision.lean, line 184
MonomialOrder.linearDivision_quotient_coeffsIn	theorem	MultivariatePolynomials/LinearDivision.lean, line 192
MonomialOrder.linearDivision_remainder_of_reduced	theorem	MultivariatePolynomials/LinearDivision.lean, line 202
MonomialOrder.linearDivision_quotient_of_reduced	theorem	MultivariatePolynomials/LinearDivision.lean, line 221
MonomialOrder.exists_monic_lift	theorem	MultivariatePolynomials/MonicLift.lean, line 38
Finsupp.cons_zero_le_cons_iff	theorem	MultivariatePolynomials/FirstVariableLex.lean, line 31
MonomialOrder.lex_le_cons_zero_of_le	theorem	MultivariatePolynomials/FirstVariableLex.lean, line 47
MonomialOrder.lex_degree_of_finSuccEquiv_scalar_top	theorem	MultivariatePolynomials/FirstVariableLex.lean, line 60

Quoted from the main results in formalization.yaml of FormalFrontier/multivariate-polynomials at commit 724d9804, Apache-2.0.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.