SchwartzZippel

📁 Source: Mathlib/Algebra/MvPolynomial/SchwartzZippel.lean

Statistics

Metric	Count
Definitions	0
Theorems schwartz_zippel_sum_degreeOf, schwartz_zippel_sup_sum, schwartz_zippel_totalDegree	3
Total	3

MvPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
schwartz_zippel_sum_degreeOf 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat NNRat.instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Finset.card Finset.filter DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fintype.piFinset Fin.fintype Finset.prod CommSemiring.toCommMonoid instCommSemiringNNRat Finset.univ Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring degreeOf	—	schwartz_zippel_sup_sum Finset.sup_le Finset.sum_le_sum IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.mono_cast IsStrictOrderedRing.toZeroLEOneClass monomial_le_degreeOf Nat.cast_nonneg'
schwartz_zippel_sup_sum 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat NNRat.instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Finset.card Finset.filter DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fintype.piFinset Fin.fintype Finset.prod CommSemiring.toCommMonoid instCommSemiringNNRat Finset.univ Finset.sup Finsupp Nat.instMulZeroClass Lattice.toSemilatticeSup NNRat.instOrderBot support Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Finsupp.instFunLike	—	eq_C_of_isEmpty Fin.isEmpty' Finset.filter.congr_simp eval_C C_ne_zero Fintype.piFinset_of_isEmpty Finset.univ_unique Finset.filter_false CharP.cast_eq_zero CharP.ofCharZero NNRat.instCharZero Finset.prod_congr Finset.univ_eq_empty div_one Finset.sum_congr NNRat.instCanonicallyOrderedAdd EmbeddingLike.map_ne_zero_iff EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass add_div Nat.cast_add Finset.card_union_add_card_inter Finset.filter_union_right Finset.filter_and add_zero add_le_add IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing instIsStrictOrderedRingNNRat covariant_swap_add_of_covariant_add div_le_div_of_nonneg_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Nat.mono_cast IsStrictOrderedRing.toZeroLEOneClass Finset.card_le_card Finset.monotone_filter_right zero_le Finset.card_consEquiv_filter_piFinset Fin.prod_univ_succ Fin.tail_def Nat.cast_zero mul_div_mul_left_le Finset.filter_filter Finset.filter_piFinset_eq_map_consEquiv Finset.filter_map Finset.card_map Finset.product_eq_biUnion_right Finset.filter_biUnion Finset.filter_image Finset.card_biUnion_le Finset.sum_le_sum Nat.instIsOrderedAddMonoid Finset.card_image_le Polynomial.natDegree_map_of_leadingCoeff_ne_zero Finset.mem_filter Polynomial.leadingCoeff.eq_1 Polynomial.natDegree_zero Polynomial.coeff_map Polynomial.coeff_zero eval_eq_eval_mv_eval' Multiset.toFinset_card_le Polynomial.card_roots' Nat.instCanonicallyOrderedAdd mem_support_coeff_finSuccEquiv mem_support_iff leadingCoeff_toLex Zero.instNonempty AddMonoidAlgebra.leadingCoeff_ne_zero Equiv.injective monomial_le_degreeOf Finset.sum_le_sum_of_subset_of_nonneg Finset.filter_subset Finset.sum_const Fintype.card_piFinset mul_comm mul_div_mul_right_le Finset.sup_add IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le NNRat.instOrderedSub support_nonempty Finset.sup_le Finset.le_sup_of_le Fin.sum_univ_succ add_comm add_le_add_left natDegree_finSuccEquiv Nat.cast_nonneg'
schwartz_zippel_totalDegree 📖	mathematical	—	NNRat Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderNNRat NNRat.instDiv AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Finset.card Finset.filter DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike eval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Fintype.piFinset Fin.fintype Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero totalDegree	—	Finset.prod_const Fintype.card_fin schwartz_zippel_sup_sum Finset.eq_empty_or_nonempty Finset.sum_congr CharP.cast_eq_zero CharP.ofCharZero NNRat.instCharZero div_zero Finset.sum_const_zero NNRat.instCanonicallyOrderedAdd Finset.sup_bot Nat.cast_finsetSup instIsStrictOrderedRingNNRat Finset.sup_div₀ le_of_lt Nat.cast_pos' IsOrderedAddMonoid.toAddLeftMono IsOrderedRing.toIsOrderedAddMonoid IsStrictOrderedRing.toIsOrderedRing IsStrictOrderedRing.toZeroLEOneClass NeZero.charZero_one Finset.Nonempty.card_pos Finsupp.sum_fintype Nat.cast_sum

---

← Back to Index