BigOperators

📁 Source: Mathlib/Algebra/Polynomial/BigOperators.lean

Statistics

Metric	Count
Definitions	0
Theorems coeff_list_prod_of_natDegree_le, coeff_multiset_prod_of_natDegree_le, coeff_prod_of_natDegree_le, coeff_zero_multiset_prod, coeff_zero_prod, degree_list_prod, degree_list_prod_le, degree_list_sum_le, degree_list_sum_le_of_forall_degree_le, degree_multiset_prod, degree_multiset_prod_le, degree_multiset_prod_of_monic, degree_prod, degree_prod_le, degree_prod_of_monic, degree_sum_eq_of_linearIndepOn, leadingCoeff_multiset_prod, leadingCoeff_multiset_prod', leadingCoeff_prod, leadingCoeff_prod', leadingCoeff_sum_of_degree_eq, multiset_prod_X_sub_C_coeff_card_pred, multiset_prod_X_sub_C_nextCoeff, natDegree_finset_prod_X_sub_C_eq_card, natDegree_list_prod_le, natDegree_list_sum_le, natDegree_multiset_prod, natDegree_multiset_prod', natDegree_multiset_prod_X_sub_C_eq_card, natDegree_multiset_prod_le, natDegree_multiset_prod_of_monic, natDegree_multiset_sum_le, natDegree_prod, natDegree_prod', natDegree_prod_le, natDegree_prod_of_monic, natDegree_sum_eq_of_linearIndepOn, natDegree_sum_le, natDegree_sum_le_of_forall_le, prod_X_sub_C_coeff_card_pred, prod_X_sub_C_nextCoeff	41
Total	41

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_list_prod_of_natDegree_le 📖	mathematical	natDegree	coeff Polynomial instMul instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	MulZeroClass.zero_mul coeff_one_zero add_mul Distrib.rightDistribClass one_mul add_comm mul_comm LE.le.trans natDegree_list_prod_le List.sum_le_card_nsmul covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid coeff_mul_add_eq_of_natDegree_le
coeff_multiset_prod_of_natDegree_le 📖	mathematical	natDegree CommSemiring.toSemiring	coeff CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.card Multiset.map	—	coeff_list_prod_of_natDegree_le
coeff_prod_of_natDegree_le 📖	mathematical	natDegree CommSemiring.toSemiring	coeff CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.card	—	Multiset.card_map Multiset.map_map Multiset.map_congr coeff_multiset_prod_of_natDegree_le
coeff_zero_multiset_prod 📖	mathematical	—	coeff CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.map	—	Multiset.induction_on coeff_one_zero Multiset.prod_cons Multiset.map_cons mul_coeff_zero
coeff_zero_prod 📖	mathematical	—	coeff CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring	—	Multiset.map_map Multiset.map_congr coeff_zero_multiset_prod
degree_list_prod 📖	mathematical	—	degree Polynomial instMul instOne WithBot WithBot.add WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	map_list_prod MonoidHom.instMonoidHomClass
degree_list_prod_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree Polynomial instMul instOne WithBot.add WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass	—	List.apply_prod_le_sum_map WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid degree_one_le degree_mul_le
degree_list_sum_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree Polynomial instAdd instZero List.maximum natDegree	—	degree_list_sum_le_of_forall_degree_le degree_eq_natDegree List.le_maximum_of_mem'
degree_list_sum_le_of_forall_degree_le 📖	mathematical	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree Polynomial instAdd instZero	—	le_trans degree_add_le max_le
degree_multiset_prod 📖	mathematical	—	degree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum WithBot WithBot.addCommMonoid Nat.instAddCommMonoid Multiset.map	—	map_multiset_prod MonoidHom.instMonoidHomClass
degree_multiset_prod_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum WithBot.addCommMonoid Nat.instAddCommMonoid Multiset.map	—	degree_list_prod_le
degree_multiset_prod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	degree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum WithBot WithBot.addCommMonoid Nat.instAddCommMonoid Multiset.map	—	Monic.ne_zero Multiset.map_id' monic_multiset_prod_of_monic degree_eq_natDegree natDegree_multiset_prod_of_monic Nat.cast_multiset_sum Multiset.map_map Multiset.map_congr
degree_prod 📖	mathematical	—	degree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum WithBot WithBot.addCommMonoid Nat.instAddCommMonoid	—	map_prod MonoidHom.instMonoidHomClass
degree_prod_le 📖	mathematical	—	WithBot Preorder.toLE WithBot.instPreorder Nat.instPreorder degree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum WithBot.addCommMonoid Nat.instAddCommMonoid	—	Multiset.map_map degree_multiset_prod_le
degree_prod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	degree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum WithBot WithBot.addCommMonoid Nat.instAddCommMonoid	—	Multiset.map_map Multiset.map_congr degree_multiset_prod_of_monic
degree_sum_eq_of_linearIndepOn 📖	mathematical	LinearIndepOn CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule SetLike.coe Finset Finset.instSetLike	degree CommSemiring.toSemiring CommRing.toCommSemiring Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instDistribSMul map algebraMap Finset.sup WithBot WithBot.semilatticeSup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat WithBot.instOrderBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder	—	le_antisymm LE.le.trans degree_sum_le Finset.sup_le degree_smul_le degree_map_le Finset.le_sup degree_eq_natDegree le_degree_of_ne_zero finset_sum_coeff coeff_smul smul_eq_mul coeff_map mul_comm Algebra.smul_def leadingCoeff_eq_zero linearIndepOn_finset_iff
leadingCoeff_multiset_prod 📖	mathematical	—	leadingCoeff CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.map	—	leadingCoeffHom_apply MonoidHom.map_multiset_prod Multiset.map_congr
leadingCoeff_multiset_prod' 📖	mathematical	—	leadingCoeff CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.map	—	Multiset.induction_on Monic.leadingCoeff Multiset.prod_cons Multiset.map_cons leadingCoeff_mul' right_ne_zero_of_mul
leadingCoeff_prod 📖	mathematical	—	leadingCoeff CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring	—	Multiset.map_map Multiset.map_congr leadingCoeff_multiset_prod
leadingCoeff_prod' 📖	mathematical	—	leadingCoeff CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring	—	Multiset.map_map Multiset.map_congr leadingCoeff_multiset_prod'
leadingCoeff_sum_of_degree_eq 📖	mathematical	degree	leadingCoeff Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring	—	Finset.sum_congr Finset.sum_const_zero natDegree_eq_of_degree_eq_some natDegree_eq_of_le_of_coeff_ne_zero natDegree_sum_le_of_forall_le instReflLe finset_sum_coeff
multiset_prod_X_sub_C_coeff_card_pred 📖	mathematical	Multiset.card	coeff CommSemiring.toSemiring CommRing.toCommSemiring Multiset.prod Polynomial CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Multiset.card NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim nextCoeff.eq_1 natDegree_multiset_prod_of_monic monic_X_sub_C Nat.instCanonicallyOrderedAdd Nat.instIsOrderedAddMonoid Multiset.card_pos_iff_exists_mem one_ne_zero natDegree_X_sub_C Multiset.map_map Multiset.map_congr natDegree_sub_C natDegree_X Multiset.map_const' Multiset.sum_replicate mul_one multiset_prod_X_sub_C_nextCoeff
multiset_prod_X_sub_C_nextCoeff 📖	mathematical	—	nextCoeff CommSemiring.toSemiring CommRing.toCommSemiring Multiset.prod Polynomial CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Multiset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Monic.nextCoeff_multiset_prod monic_X_sub_C Multiset.map_congr nextCoeff_X_sub_C Multiset.sum_hom AddMonoidHom.instAddMonoidHomClass
natDegree_finset_prod_X_sub_C_eq_card 📖	mathematical	—	natDegree CommSemiring.toSemiring CommRing.toCommSemiring Finset.prod Polynomial CommRing.toCommMonoid commRing instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Finset.card	—	Finset.prod.eq_1 Multiset.map_map natDegree_multiset_prod_X_sub_C_eq_card Multiset.card_map Finset.card.eq_1
natDegree_list_prod_le 📖	mathematical	—	natDegree Polynomial instMul instOne MulZeroClass.toZero Nat.instMulZeroClass	—	List.apply_prod_le_sum_map IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Eq.le natDegree_one natDegree_mul_le
natDegree_list_sum_le 📖	mathematical	—	natDegree Polynomial instAdd instZero	—	List.sum_le_foldr_max instReflLe natDegree_add_le
natDegree_multiset_prod 📖	mathematical	Polynomial CommSemiring.toSemiring Multiset Multiset.instMembership instZero	natDegree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum Nat.instAddCommMonoid Multiset.map	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_of_subsingleton Multiset.map_congr Multiset.map_const' Multiset.sum_replicate nsmul_zero natDegree_multiset_prod'
natDegree_multiset_prod' 📖	mathematical	—	natDegree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum Nat.instAddCommMonoid Multiset.map	—	Multiset.induction_on natDegree_one Multiset.map_cons Multiset.prod_cons Multiset.sum_cons natDegree_mul' leadingCoeff_multiset_prod' right_ne_zero_of_mul
natDegree_multiset_prod_X_sub_C_eq_card 📖	mathematical	—	natDegree CommSemiring.toSemiring CommRing.toCommSemiring Multiset.prod Polynomial CommRing.toCommMonoid commRing Multiset.map instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Multiset.card	—	natDegree_multiset_prod_of_monic Multiset.forall_mem_map_iff monic_X_sub_C Multiset.map_map Multiset.map_congr natDegree_sub_C natDegree_X Multiset.map_const' Multiset.sum_replicate mul_one
natDegree_multiset_prod_le 📖	mathematical	—	natDegree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum Nat.instAddCommMonoid Multiset.map	—	natDegree_list_prod_le
natDegree_multiset_prod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	natDegree CommSemiring.toSemiring Multiset.prod Polynomial CommSemiring.toCommMonoid commSemiring Multiset.sum Nat.instAddCommMonoid Multiset.map	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_of_subsingleton Multiset.map_congr Multiset.map_const' Multiset.sum_replicate nsmul_zero natDegree_multiset_prod' Monic.leadingCoeff Multiset.prod_replicate one_pow NeZero.one
natDegree_multiset_sum_le 📖	mathematical	—	natDegree Multiset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Multiset.foldr instLeftCommutativeOfCommutativeOfAssociative Multiset.map	—	instLeftCommutativeOfCommutativeOfAssociative natDegree_list_sum_le
natDegree_prod 📖	mathematical	—	natDegree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum Nat.instAddCommMonoid	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_of_subsingleton Finset.sum_congr Finset.sum_const_zero natDegree_prod' Finset.prod_ne_zero_iff
natDegree_prod' 📖	mathematical	—	natDegree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum Nat.instAddCommMonoid	—	Multiset.map_map Multiset.map_congr natDegree_multiset_prod'
natDegree_prod_le 📖	mathematical	—	natDegree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum Nat.instAddCommMonoid	—	Multiset.map_map Multiset.map_congr natDegree_multiset_prod_le
natDegree_prod_of_monic 📖	mathematical	Monic CommSemiring.toSemiring	natDegree CommSemiring.toSemiring Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum Nat.instAddCommMonoid	—	Multiset.map_map Multiset.map_congr natDegree_multiset_prod_of_monic
natDegree_sum_eq_of_linearIndepOn 📖	mathematical	LinearIndepOn CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule SetLike.coe Finset Finset.instSetLike	natDegree CommSemiring.toSemiring CommRing.toCommSemiring Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing SMulZeroClass.toSMul instZero smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing instDistribSMul map algebraMap Finset.sup Lattice.toSemilatticeSup DistribLattice.toLattice instDistribLatticeNat Nat.instOrderBot	—	le_antisymm natDegree_sum_le_of_forall_le LE.le.trans natDegree_smul_le natDegree_map_le Finset.le_sup Finset.sup_le Nat.instCanonicallyOrderedAdd le_natDegree_of_ne_zero finset_sum_coeff coeff_smul smul_eq_mul coeff_map mul_comm Algebra.smul_def leadingCoeff_eq_zero linearIndepOn_finset_iff
natDegree_sum_le 📖	mathematical	—	natDegree Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring Finset.fold	—	Finset.fold_congr instLeftCommutativeOfCommutativeOfAssociative Multiset.foldr.congr_simp Multiset.map_map Multiset.map_congr natDegree_multiset_sum_le
natDegree_sum_le_of_forall_le 📖	mathematical	natDegree	natDegree Finset.sum Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring	—	le_trans natDegree_sum_le instCommutativeMax instAssociativeMax Finset.fold_max_le Nat.instCanonicallyOrderedAdd
prod_X_sub_C_coeff_card_pred 📖	mathematical	Finset.card	coeff CommSemiring.toSemiring CommRing.toCommSemiring Finset.prod Polynomial CommRing.toCommMonoid commRing instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Finset.card NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Multiset.map_map Multiset.map_congr Multiset.card_map multiset_prod_X_sub_C_coeff_card_pred
prod_X_sub_C_nextCoeff 📖	mathematical	—	nextCoeff CommSemiring.toSemiring CommRing.toCommSemiring Finset.prod Polynomial CommRing.toCommMonoid commRing instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Multiset.map_map Multiset.map_congr multiset_prod_X_sub_C_nextCoeff

---

← Back to Index