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, 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_le, natDegree_sum_le_of_forall_le, prod_X_sub_C_coeff_card_pred, prod_X_sub_C_nextCoeff	39
Total	39

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 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 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	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 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 Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum WithBot WithBot.addCommMonoid Nat.instAddCommMonoid	—	Multiset.map_map Multiset.map_congr degree_multiset_prod_of_monic
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 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 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 natDegree_add_le
natDegree_multiset_prod 📖	mathematical	Polynomial CommSemiring.toSemiring Multiset Multiset.instMembership instZero	natDegree Multiset.prod 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_X_sub_C 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 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 Finset.prod Polynomial CommSemiring.toCommMonoid commSemiring Finset.sum Nat.instAddCommMonoid	—	Multiset.map_map Multiset.map_congr natDegree_multiset_prod_of_monic
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	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 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