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 Finset.instMembership	—	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 AddLeftCancelSemigroup.toIsLeftCancelAdd Finsupp.single_eq_same covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd Nat.instCanonicallyOrderedAdd
combinatorial_nullstellensatz_exists_linearCombination 📖	mathematical	Finset.Nonempty DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	totalDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib instCommRingMvPolynomial Finset.prod CommRing.toCommMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing X C Finsupp Finsupp.instFunLike LinearMap RingHom.id NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid 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 Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	instCommRingMvPolynomial	—	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