Nullstellensatz

📁 Source: Mathlib/Combinatorics/Nullstellensatz.lean

Statistics

Metric	Count
Definitions	0
Theorems combinatorial_nullstellensatz_exists_eval_nonzero, combinatorial_nullstellensatz_exists_linearCombination, eq_zero_of_eval_zero_at_prod_finset	3
Total	3

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
combinatorial_nullstellensatz_exists_eval_nonzero 📖	mathematical	totalDegree CommRing.toCommSemiring DFunLike.coe AddMonoidHom Finsupp AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Nat.instAddCommMonoid Finsupp.instAddZeroClass AddMonoidHom.instFunLike Finsupp.degree MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instFunLike Finset.card	Finset SetLike.instMembership Finset.instSetLike	—	WellOrderingRel.isWellOrder combinatorial_nullstellensatz_exists_linearCombination Finset.card_pos Mathlib.Tactic.Push.not_and_eq Finsupp.linearCombination_apply Finsupp.sum.eq_1 coeff_sum Finset.sum_eq_zero MulZeroClass.zero_mul mul_comm smul_eq_mul coeff_mul IsDomain.to_noZeroDivisors mem_support_iff coeff_eq_zero_of_totalDegree_lt Finsupp.degree_apply lt_of_add_lt_add_right contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid lt_of_le_of_lt Finsupp.degree_single IsWellOrder.toIsWellFounded isWellOrder_gt Finite.to_wellFoundedGT degree_degLexDegree map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass IsDomain.toNontrivial MonomialOrder.degree_mul_of_isRegular_right MonomialOrder.Monic.leadingCoeff_eq_one add_lt_add_iff_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid Finsupp.single_eq_same covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT instIsRightCancelAddOfAddRightReflectLE IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT Nat.instCanonicallyOrderedAdd
combinatorial_nullstellensatz_exists_linearCombination 📖	mathematical	Finset.Nonempty DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	Finsupp MvPolynomial CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid totalDegree AddMonoidAlgebra.instMul Finset.prod CommRing.toCommMonoid AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring CommRing.toRing Finsupp.instAddMonoid X DFunLike.coe RingHom Semiring.toNonAssocSemiring AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass RingHom.instFunLike C Finsupp.instFunLike LinearMap AddMonoidAlgebra.semiring RingHom.id NonAssocSemiring.toNonUnitalNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid AddMonoidAlgebra.addAddCommMonoid Finsupp.module Semiring.toModule LinearMap.instFunLike Finsupp.linearCombination	—	WellOrderingRel.isWellOrder IsWellOrder.toIsWellFounded isWellOrder_gt Finite.to_wellFoundedGT MonomialOrder.div MonomialOrder.Monic.leadingCoeff_eq_one IsDomain.toNontrivial eq_zero_of_eval_zero_at_prod_finset degreeOf_eq_sup Finset.sup_lt_iff not_le Finsupp.single_apply zero_le Nat.instCanonicallyOrderedAdd sub_eq_iff_eq_add' map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass zero_sub neg_eq_zero Finsupp.linearCombination_apply map_finsuppSum Finsupp.sum.eq_1 Finset.sum_eq_zero smul_eq_mul map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass Finset.prod_eq_zero eval_X eval_C sub_self MulZeroClass.mul_zero degLex_totalDegree_monotone add_zero
eq_zero_of_eval_zero_at_prod_finset 📖	mathematical	degreeOf CommRing.toCommSemiring Finset.card DFunLike.coe RingHom MvPolynomial AddMonoidAlgebra.nonAssocSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring RingHom.instFunLike eval NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	MvPolynomial CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Nat.instAddMonoid	—	Finite.induction_empty_option Equiv.symm_apply_apply degreeOf_rename_of_injective Equiv.injective eval_rename Equiv.apply_symm_apply rename_injective AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.injective_iff_ker_eq_bot RingHom.mem_ker ext Finsupp.ext coeff_C PEmpty.instIsEmpty eval_C C_0 Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero' optionEquivLeft_elim_eval lt_of_le_of_lt Polynomial.natDegree_le_iff_coeff_eq_zero coeff_eval_eq_eval_coeff Finsupp.eq_option_embedding_update_none_iff optionEquivLeft_coeff_some_coeff_none not_le degreeOf_eq_sup Finset.le_sup mem_support_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Polynomial.ext Finsupp.some_apply Polynomial.coeff_map Polynomial.ext_iff AlgEquiv.symm_apply_apply AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass

---

← Back to Index