Bernstein

📁 Source: Mathlib/RingTheory/Polynomial/Bernstein.lean

Statistics

Metric	Count
Definitions bernsteinPolynomial	1
Theorems derivative_succ, derivative_succ_aux, derivative_zero, eq_zero_of_lt, eval_at_0, eval_at_1, flip, flip', iterate_derivative_at_0, iterate_derivative_at_0_eq_zero_of_lt, iterate_derivative_at_0_ne_zero, iterate_derivative_at_1, iterate_derivative_at_1_eq_zero_of_lt, iterate_derivative_at_1_ne_zero, iterate_derivative_succ_at_0_eq_zero, linearIndependent, linearIndependent_aux, map, sum, sum_mul_smul, sum_smul, variance	22
Total	23

(root)

Definitions

Name	Category	Theorems
bernsteinPolynomial 📖	CompOp	20 math math: bernsteinPolynomial.eval_at_1, bernsteinPolynomial.iterate_derivative_at_1_eq_zero_of_lt, bernsteinPolynomial.flip', bernsteinPolynomial.flip, bernsteinPolynomial.variance, bernsteinPolynomial.sum_smul, bernsteinPolynomial.iterate_derivative_succ_at_0_eq_zero, bernsteinPolynomial.linearIndependent_aux, bernsteinPolynomial.sum_mul_smul, bernsteinPolynomial.eq_zero_of_lt, bernsteinPolynomial.derivative_succ, bernsteinPolynomial.eval_at_0, bernsteinPolynomial.map, bernsteinPolynomial.sum, bernsteinPolynomial.linearIndependent, bernsteinPolynomial.derivative_zero, bernsteinPolynomial.iterate_derivative_at_0_eq_zero_of_lt, bernsteinPolynomial.iterate_derivative_at_0, bernsteinPolynomial.derivative_succ_aux, bernsteinPolynomial.iterate_derivative_at_1

bernsteinPolynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
derivative_succ 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial Polynomial.instMul Polynomial.instNatCast Polynomial.instSub CommRing.toRing	—	Nat.cast_zero MulZeroClass.zero_mul zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one Polynomial.derivative_zero sub_zero Nat.cast_succ derivative_succ_aux
derivative_succ_aux 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial Polynomial.instMul Polynomial.instAdd Polynomial.instNatCast Polynomial.instOne Polynomial.instSub CommRing.toRing	—	eq_1 mul_sub Nat.cast_mul Nat.cast_add Nat.cast_one Nat.add_one_mul_choose_eq tsub_add_eq_tsub_tsub Nat.instOrderedSub mul_assoc mul_comm Nat.choose_mul_succ_eq Polynomial.derivative_mul Polynomial.derivative_natCast MulZeroClass.zero_mul Polynomial.derivative_pow map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass map_natCast map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Polynomial.derivative_X mul_one zero_add Polynomial.derivative_sub Polynomial.derivative_one zero_sub mul_neg
derivative_zero 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial Polynomial.instMul Polynomial.instNeg CommRing.toRing Polynomial.instNatCast	—	Nat.choose_zero_right Nat.cast_one pow_zero mul_one tsub_zero Nat.instOrderedSub one_mul Polynomial.derivative_pow map_natCast RingHom.instRingHomClass Polynomial.derivative_sub Polynomial.derivative_one Polynomial.derivative_X zero_sub mul_neg neg_mul
eq_zero_of_lt 📖	mathematical	—	bernsteinPolynomial Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero	—	Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul
eval_at_0 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing bernsteinPolynomial AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	eq_1 Nat.choose_zero_right Nat.cast_one pow_zero mul_one tsub_zero Nat.instOrderedSub one_mul Polynomial.eval_pow Polynomial.eval_sub Polynomial.eval_one Polynomial.eval_X sub_zero one_pow Polynomial.eval_mul Polynomial.eval_natCast zero_pow MulZeroClass.mul_zero
eval_at_1 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing bernsteinPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	eq_1 Nat.choose_self Nat.cast_one one_mul tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one Polynomial.eval_pow Polynomial.eval_X one_pow Ne.lt_or_gt Polynomial.eval_mul Polynomial.eval_natCast Polynomial.eval_sub Polynomial.eval_one sub_self zero_pow MulZeroClass.mul_zero Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.zero_mul Polynomial.eval_zero
flip 📖	mathematical	—	Polynomial.comp CommSemiring.toSemiring CommRing.toCommSemiring bernsteinPolynomial Polynomial Polynomial.instSub CommRing.toRing Polynomial.instOne Polynomial.X	—	Polynomial.mul_comp Polynomial.natCast_comp Polynomial.pow_comp Polynomial.X_comp Polynomial.sub_comp Polynomial.one_comp sub_sub_cancel mul_right_comm Nat.choose_symm tsub_tsub_assoc CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le tsub_self zero_add
flip' 📖	mathematical	—	bernsteinPolynomial Polynomial.comp CommSemiring.toSemiring CommRing.toCommSemiring Polynomial Polynomial.instSub CommRing.toRing Polynomial.instOne Polynomial.X	—	flip Polynomial.comp_assoc Polynomial.sub_comp Polynomial.one_comp Polynomial.X_comp sub_sub_cancel Polynomial.comp_X
iterate_derivative_at_0 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing ascPochhammer	—	eval_at_0 zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub tsub_zero Polynomial.eval_one le_tsub_of_add_le_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid derivative_succ Polynomial.iterate_derivative_natCast_mul Polynomial.iterate_derivative_sub Polynomial.eval_mul Polynomial.eval_natCast Polynomial.eval_sub iterate_derivative_succ_at_0_eq_zero sub_zero ascPochhammer_succ_left Polynomial.eval_X Polynomial.eval_comp Polynomial.eval_add mul_one ascPochhammer_eval_succ Nat.cast_mul ascPochhammer_eval_cast tsub_add_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE LE.le.trans tsub_eq_zero_iff_le eq_zero_of_lt iterate_map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Polynomial.eval_zero Nat.cast_zero ascPochhammer_ne_zero_eval_zero pos_iff_ne_zero pos_of_gt
iterate_derivative_at_0_eq_zero_of_lt 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial	—	Nat.instCanonicallyOrderedAdd eval_at_0 derivative_succ Polynomial.iterate_derivative_natCast_mul Polynomial.iterate_derivative_sub Polynomial.eval_mul Polynomial.eval_natCast Polynomial.eval_sub mul_eq_zero_of_right sub_zero LT.lt.trans_le
iterate_derivative_at_0_ne_zero 📖	—	—	—	—	iterate_derivative_at_0 Nat.cast_zero ne_of_gt zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub tsub_zero Polynomial.eval_one Nat.instZeroLEOneClass ascPochhammer_pos Nat.instIsStrictOrderedRing tsub_pos_of_lt
iterate_derivative_at_1 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Distrib.toAdd AddMonoidWithOne.toNatCast ascPochhammer	—	flip' Polynomial.iterate_derivative_comp_one_sub_X Polynomial.eval_mul Polynomial.eval_pow Polynomial.eval_neg Polynomial.eval_one Polynomial.eval_comp Polynomial.eval_sub Polynomial.eval_X sub_self iterate_derivative_at_0 LE.le.eq_or_lt tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero zero_tsub tsub_zero mul_one Nat.cast_one
iterate_derivative_at_1_eq_zero_of_lt 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	flip' LT.lt.le tsub_pos_iff_lt Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pos_of_gt Polynomial.iterate_derivative_comp_one_sub_X Polynomial.eval_mul Polynomial.eval_pow Polynomial.eval_neg Polynomial.eval_one Polynomial.eval_comp Polynomial.eval_sub Polynomial.eval_X sub_self iterate_derivative_at_0_eq_zero_of_lt MulZeroClass.mul_zero
iterate_derivative_at_1_ne_zero 📖	—	—	—	—	iterate_derivative_at_1 neg_one_pow_mul_eq_zero_iff Nat.cast_succ ascPochhammer_eval_cast Nat.cast_zero LT.lt.ne' ascPochhammer_pos Nat.instIsStrictOrderedRing
iterate_derivative_succ_at_0_eq_zero 📖	mathematical	—	Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Nat.iterate Polynomial DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Polynomial.module Semiring.toModule LinearMap.instFunLike Polynomial.derivative bernsteinPolynomial	—	iterate_derivative_at_0_eq_zero_of_lt lt_add_one Nat.instZeroLEOneClass IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid
linearIndependent 📖	mathematical	—	LinearIndependent Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing bernsteinPolynomial Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.module Semiring.toModule	—	linearIndependent_aux le_rfl
linearIndependent_aux 📖	mathematical	—	LinearIndependent Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Rat.commRing bernsteinPolynomial Rat.semiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.module Semiring.toModule	—	linearIndependent_empty_type Fin.isEmpty' linearIndependent_fin_succ' le_of_lt Submodule.notMem_span_of_apply_notMem_span_image RingHomSurjective.ids Submodule.span_image Module.End.pow_apply Submodule.span_induction iterate_derivative_at_1_eq_zero_of_lt tsub_lt_tsub_iff_left_of_le Nat.instCanonicallyOrderedAdd Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add IsRightCancelAdd.addRightReflectLE_of_addRightReflectLT AddRightCancelSemigroup.toIsRightCancelAdd contravariant_swap_add_of_contravariant_add iterate_map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Polynomial.eval_zero iterate_map_add SemilinearMapClass.toAddHomClass Polynomial.eval_add add_zero Polynomial.iterate_derivative_smul IsScalarTower.right Polynomial.eval_smul MulZeroClass.mul_zero iterate_derivative_at_1_ne_zero Rat.instCharZero
map 📖	mathematical	—	Polynomial.map CommSemiring.toSemiring CommRing.toCommSemiring bernsteinPolynomial	—	Polynomial.map_mul Polynomial.map_natCast Polynomial.map_pow Polynomial.map_X Polynomial.map_sub Polynomial.map_one
sum 📖	mathematical	—	Finset.sum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Finset.range bernsteinPolynomial Polynomial.instOne	—	add_pow Finset.sum_congr mul_assoc mul_comm add_sub_cancel one_pow
sum_mul_smul 📖	mathematical	—	Finset.sum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Finset.range Polynomial.instNSMul bernsteinPolynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	MvPolynomial.pderiv_X zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub MulZeroClass.mul_zero zero_nsmul Nat.choose_zero_right Nat.cast_one tsub_zero Nat.cast_zero pow_zero mul_one MulZeroClass.zero_mul zero_add tsub_self Nat.choose_one_right eq_1 add_zero pow_succ Nat.cast_mul Nat.cast_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_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.add_pf_add_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_atom Mathlib.Tactic.Ring.cast_zero add_pow map_sum Derivation.instAddMonoidHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Finset.sum_mul Finset.sum_congr Derivation.leibniz Derivation.map_natCast Derivation.leibniz_pow smul_zero nsmul_eq_mul map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_natCast AlgHomClass.toRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MvPolynomial.aeval_X Derivation.map_add map_nsmul smul_smul map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass add_sub_cancel one_pow smul_one_mul IsScalarTower.right
sum_smul 📖	mathematical	—	Finset.sum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Finset.range Polynomial.instNSMul bernsteinPolynomial Polynomial.X	—	MvPolynomial.pderiv_X zero_nsmul Nat.cast_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub pow_zero mul_one tsub_zero MulZeroClass.zero_mul Nat.choose_zero_right Nat.cast_one eq_1 pow_succ add_zero Nat.cast_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_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_congr Mathlib.Tactic.Ring.pow_add 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.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_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_atom add_pow map_sum Derivation.instAddMonoidHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Finset.sum_mul Finset.sum_congr MvPolynomial.pderiv_mul Derivation.leibniz_pow nsmul_eq_mul MulZeroClass.mul_zero smul_zero Derivation.map_natCast map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_natCast AlgHomClass.toRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MvPolynomial.aeval_X Derivation.map_add map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass add_sub_cancel one_pow
variance 📖	mathematical	—	Finset.sum Polynomial CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Finset.range Polynomial.instMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.instSub CommRing.toRing Polynomial.instNSMul Polynomial.X Polynomial.instNatCast bernsteinPolynomial Polynomial.instOne	—	Finset.sum_congr Nat.instAtLeastTwoHAddOfNat Nat.cast_mul Nat.cast_pow Nat.cast_zero sub_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub MulZeroClass.mul_zero add_zero zero_add Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Nat.cast_add Nat.cast_one add_tsub_cancel_right IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add 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_mul Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_nat Mathlib.Tactic.Ring.coeff_one Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_bit0 Mathlib.Tactic.Ring.pow_one Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.instAtLeastTwo sum sum_smul sum_mul_smul Polynomial.natCast_mul Finset.mul_sum Finset.sum_add_distrib Distrib.rightDistribClass MulZeroClass.zero_mul zero_pow Nat.instCharZero mul_one Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero

---

← Back to Index