MulCoeff

📁 Source: Mathlib/RingTheory/WittVector/MulCoeff.lean

Statistics

Metric	Count
Definitions nthRemainder, polyOfInterest, remainder, wittPolyProd, wittPolyProdRemainder	5
Theorems mul_polyOfInterest_aux1, mul_polyOfInterest_aux2, mul_polyOfInterest_aux3, mul_polyOfInterest_aux4, mul_polyOfInterest_aux5, mul_polyOfInterest_vars, nthRemainder_spec, nth_mul_coeff, nth_mul_coeff', peval_polyOfInterest, peval_polyOfInterest', polyOfInterest_vars, polyOfInterest_vars_eq, remainder_vars, wittPolyProdRemainder_vars, wittPolyProd_vars	16
Total	21

WittVector

Definitions

Name	Category	Theorems
nthRemainder 📖	CompOp	2 math math: RecursionMain.succNthVal_spec', nthRemainder_spec
polyOfInterest 📖	CompOp	6 math math: mul_polyOfInterest_vars, polyOfInterest_vars, polyOfInterest_vars_eq, mul_polyOfInterest_aux5, peval_polyOfInterest', peval_polyOfInterest
remainder 📖	CompOp	4 math math: remainder_vars, mul_polyOfInterest_aux4, mul_polyOfInterest_aux5, mul_polyOfInterest_aux3
wittPolyProd 📖	CompOp	4 math math: mul_polyOfInterest_aux2, mul_polyOfInterest_aux1, mul_polyOfInterest_aux3, wittPolyProd_vars
wittPolyProdRemainder 📖	CompOp	4 math math: mul_polyOfInterest_aux2, mul_polyOfInterest_aux4, mul_polyOfInterest_aux5, wittPolyProdRemainder_vars

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_polyOfInterest_aux1 📖	mathematical	—	Finset.sum MvPolynomial Int.instCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Finset.range Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing wittMul Nat.instMonoid wittPolyProd	—	Finset.sum_congr map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass MvPolynomial.ext Finsupp.support_eq_singleton Finsupp.single_eq_same pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Nat.Prime.ne_zero Fact.out MvPolynomial.bind₁_monomial eq_intCast RingHom.instRingHomClass Int.cast_pow Int.cast_natCast Finset.prod_congr Finset.prod_singleton map_mul NonUnitalAlgSemiHomClass.toMulHomClass MvPolynomial.bind₁_X_right wittStructureInt_prop
mul_polyOfInterest_aux2 📖	mathematical	—	MvPolynomial Int.instCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing wittMul wittPolyProdRemainder wittPolyProd	—	Finset.sum_range_succ add_comm pow_zero pow_one mul_polyOfInterest_aux1
mul_polyOfInterest_aux3 📖	mathematical	—	wittPolyProd MvPolynomial Int.instCommSemiring Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Distrib.toMul NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MvPolynomial.X CommRing.toCommSemiring DFunLike.coe AlgHom MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename wittPolynomial remainder	—	wittPolyProd.eq_1 wittPolynomial.eq_1 map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Finset.sum_range_succ MvPolynomial.C_mul_X_pow_eq_monomial tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero pow_one map_mul NonUnitalAlgSemiHomClass.toMulHomClass MvPolynomial.rename_C MvPolynomial.rename_X mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass add_comm add_assoc Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
mul_polyOfInterest_aux4 📖	mathematical	—	MvPolynomial Int.instCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing wittMul Distrib.toAdd NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup MvPolynomial.X CommRing.toCommSemiring DFunLike.coe AlgHom MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename wittPolynomial SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup remainder wittPolyProdRemainder	—	add_sub_assoc eq_sub_iff_add_eq mul_polyOfInterest_aux2 mul_polyOfInterest_aux3
mul_polyOfInterest_aux5 📖	mathematical	—	MvPolynomial Int.instCommSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing polyOfInterest SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup remainder wittPolyProdRemainder	—	mul_sub mul_add Distrib.leftDistribClass mul_polyOfInterest_aux4 Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
mul_polyOfInterest_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing polyOfInterest SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	mul_polyOfInterest_aux5 Finset.Subset.trans MvPolynomial.vars_sub_subset Finset.union_subset remainder_vars wittPolyProdRemainder_vars
nthRemainder_spec 📖	mathematical	—	coeff WittVector instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Nat.instMonoid nthRemainder truncateFun	—	nth_mul_coeff
nth_mul_coeff 📖	mathematical	—	coeff WittVector instMul Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Nat.instMonoid truncateFun	—	nth_mul_coeff' Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add
nth_mul_coeff' 📖	mathematical	—	truncateFun SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing coeff WittVector instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Nat.instMonoid	—	MvPolynomial.exists_restrict_to_vars polyOfInterest_vars Fintype.complete
peval_polyOfInterest 📖	mathematical	—	peval polyOfInterest Matrix.vecCons coeff Matrix.vecEmpty SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing WittVector instMul Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid Finset.range Nat.instMonoid	—	map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass MvPolynomial.aeval_X sub_sub add_comm map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass map_natCast MvPolynomial.eval₂Hom_X' Matrix.cons_val' Matrix.cons_val_fin_one wittPolynomial_eq_sum_C_mul_X_pow Finset.sum_congr RingHom.instRingHomClass map_sum MvPolynomial.rename_X mul_coeff
peval_polyOfInterest' 📖	mathematical	—	peval polyOfInterest Matrix.vecCons coeff Matrix.vecEmpty SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing WittVector instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Nat.instMonoid	—	peval_polyOfInterest CharP.cast_eq_zero zero_pow Unique.instSubsingleton MulZeroClass.zero_mul add_zero Finset.sum_congr Finset.sum_eq_single_of_mem IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial Nat.instAtLeastTwoHAddOfNat Nat.instNoMaxOrder pow_zero tsub_zero Nat.instOrderedSub one_mul
polyOfInterest_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring polyOfInterest SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	polyOfInterest_vars_eq mul_polyOfInterest_vars
polyOfInterest_vars_eq 📖	mathematical	—	MvPolynomial.vars Int.instCommSemiring polyOfInterest MvPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial Int.instCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MvPolynomial.commSemiring AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Distrib.toAdd wittMul MvPolynomial.X DFunLike.coe AlgHom MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.rename wittPolynomial	—	polyOfInterest.eq_1 MvPolynomial.vars_C_mul IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE pow_ne_zero isReduced_of_noZeroDivisors Nat.cast_zero Int.instCharZero Nat.Prime.ne_zero Fact.out
remainder_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring remainder SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	remainder.eq_1 Finset.Subset.trans MvPolynomial.vars_mul Finset.union_subset MvPolynomial.vars_sum_subset Finset.biUnion_subset MvPolynomial.rename_monomial MvPolynomial.vars_monomial pow_ne_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Int.instIsStrictOrderedRing AddGroup.existsAddOfLE Nat.cast_zero Int.instCharZero Nat.Prime.ne_zero Fact.out Finsupp.mapDomain_single Finsupp.support_single_subset Nat.instNoMaxOrder Finset.mem_range
wittPolyProdRemainder_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittPolyProdRemainder SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittPolyProdRemainder.eq_1 Finset.Subset.trans MvPolynomial.vars_sum_subset Finset.biUnion_subset MvPolynomial.vars_mul Finset.union_subset MvPolynomial.vars_pow eq_intCast RingHom.instRingHomClass Int.cast_natCast MvPolynomial.vars_C Finset.empty_subset wittMul_vars Finset.product_subset_product Finset.Subset.refl Nat.instNoMaxOrder
wittPolyProd_vars 📖	mathematical	—	Finset Finset.instHasSubset MvPolynomial.vars Int.instCommSemiring wittPolyProd SProd.sprod Finset.instSProd Finset.univ Fin.fintype Finset.range	—	wittPolyProd.eq_1 Finset.Subset.trans MvPolynomial.vars_mul Finset.union_subset MvPolynomial.vars_rename wittPolynomial_vars NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Int.instCharZero Nat.instNoMaxOrder

---

← Back to Index