Taylor

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

Statistics

Metric	Count
Definitions taylor, taylorAlgHom, taylorEquiv	3
Theorems aeval_add_of_sq_eq_zero, coe_taylorAlgHom, coe_taylorEquiv, coeff_taylor_natDegree, degree_taylor, eq_zero_of_hasseDeriv_eq_zero, eval_add_of_sq_eq_zero, leadingCoeff_taylor, map_taylor, natDegree_taylor, sum_taylor_eq, taylorAlgHom_apply, taylorEquiv_symm, taylor_C, taylor_X, taylor_X_pow, taylor_apply, taylor_coeff, taylor_coeff_one, taylor_coeff_zero, taylor_eq_zero, taylor_eval, taylor_eval_sub, taylor_inj, taylor_injective, taylor_monomial, taylor_mul, taylor_one, taylor_pow, taylor_taylor, taylor_zero, taylor_zero', toAlgHom_taylorEquiv	33
Total	36

Polynomial

Definitions

Name	Category	Theorems
taylor 📖	CompOp	38 math math: taylor_eval, coe_taylorAlgHom, taylor_mul, RatFunc.laurent_algebraMap, RatFunc.laurent_div, coeff_taylor_natDegree, taylor_injective, taylor_zero', map_taylor, taylor_eq_zero, RatFunc.laurentAux_div, taylor_apply, natDegree_taylor, degree_taylor, Splits.taylor, taylor_coeff_zero, taylor_X_pow, RatFunc.laurentAux_algebraMap, taylorAlgHom_apply, resultant_taylor, taylor_taylor, taylor_coeff_one, taylor_monomial, sum_taylor_eq, taylor_eval_sub, taylor_zero, taylor_coeff, taylor_inj, RatFunc.taylor_mem_nonZeroDivisors, taylor_mem_degreeLT, taylor_X, taylor_pow, coe_taylorEquiv, RatFunc.laurentAux_ofFractionRing_mk, taylorLinearEquiv_apply_coe, taylor_C, taylor_one, leadingCoeff_taylor
taylorAlgHom 📖	CompOp	3 math math: coe_taylorAlgHom, toAlgHom_taylorEquiv, taylorAlgHom_apply
taylorEquiv 📖	CompOp	6 math math: toAlgHom_taylorEquiv, comap_taylorEquiv_degreeLT, taylorEquiv_symm, coe_taylorEquiv, taylorLinearEquiv_apply_coe, map_taylorEquiv_degreeLT

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_add_of_sq_eq_zero 📖	mathematical	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	eval_add_of_sq_eq_zero derivative_map
coe_taylorAlgHom 📖	mathematical	—	SemilinearMapClass.semilinearMap Polynomial CommSemiring.toSemiring AlgHom semiring algebraOfAlgebra Algebra.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring module Semiring.toModule RingHom.id taylorAlgHom AlgHom.funLike NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass taylor	—	NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass
coe_taylorEquiv 📖	mathematical	—	LinearEquiv.toLinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing Algebra.toModule semiring algebraOfAlgebra Algebra.id SemilinearEquivClass.semilinearEquiv AlgEquiv AlgEquiv.instEquivLike AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass taylorEquiv taylor	—	RingHomInvPair.ids AlgEquivClass.toLinearEquivClass AlgEquiv.instAlgEquivClass
coeff_taylor_natDegree 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor natDegree leadingCoeff	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass coeff_natDegree taylor_coeff hasseDeriv_natDegree_eq_C eval_C
degree_taylor 📖	mathematical	—	degree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass degree_eq_natDegree degree_eq_iff_natDegree_eq Iff.not taylor_eq_zero natDegree_taylor
eq_zero_of_hasseDeriv_eq_zero 📖	mathematical	eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike hasseDeriv MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	instZero	—	taylor_eq_zero ext taylor_coeff coeff_zero
eval_add_of_sq_eq_zero 📖	mathematical	Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	eval Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib Distrib.toMul DFunLike.coe LinearMap RingHom.id Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid semiring module Semiring.toModule LinearMap.instFunLike derivative	—	add_comm taylor_eval eval_eq_sum_range' LT.lt.trans Finset.sum_range_succ' Finset.sum_congr natDegree_taylor pow_succ mul_assoc MulZeroClass.mul_zero Finset.sum_const_zero zero_add taylor_coeff_one pow_zero one_mul taylor_coeff_zero mul_one
leadingCoeff_taylor 📖	mathematical	—	leadingCoeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor	—	leadingCoeff.eq_1 natDegree_taylor coeff_taylor_natDegree
map_taylor 📖	mathematical	—	map DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor RingHom RingHom.instFunLike	—	map_comp map_add map_X map_C
natDegree_taylor 📖	mathematical	—	natDegree DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor	—	map_natDegree_eq_natDegree DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim taylor_monomial natDegree_of_subsingleton instIsEmptyFalse natDegree_C_mul_of_mul_ne_zero leadingCoeff_pow_X_add_C mul_one natDegree_pow_X_add_C
sum_taylor_eq 📖	mathematical	—	sum CommSemiring.toSemiring CommRing.toCommSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing commRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor instMul RingHom RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSub CommRing.toRing X	—	comp_eq_sum_left sub_eq_add_neg C_neg taylor_apply taylor_taylor neg_add_cancel taylor_zero
taylorAlgHom_apply 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike taylorAlgHom LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike taylor	—	—
taylorEquiv_symm 📖	mathematical	—	AlgEquiv.symm Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id taylorEquiv NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	AlgEquiv.ext
taylor_C 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor RingHom RingHom.instFunLike C	—	C_comp
taylor_X 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor X instAdd RingHom RingHom.instFunLike C	—	X_comp
taylor_X_pow 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X instAdd RingHom RingHom.instFunLike C	—	X_pow_comp
taylor_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor comp instAdd X RingHom RingHom.instFunLike C	—	—
taylor_coeff 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor eval hasseDeriv	—	RingHomCompTriple.ids lhom_ext' LinearMap.ext_ring monomial_comp Commute.add_pow commute_X one_mul map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass hasseDeriv_monomial mul_one eval_monomial Finset.sum_congr mul_assoc coeff_mul_C coeff_X_pow boole_mul Finset.sum_ite_eq Commute.eq Nat.cast_commute Nat.choose_eq_zero_of_lt Nat.cast_zero MulZeroClass.mul_zero
taylor_coeff_one 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor eval derivative	—	taylor_coeff hasseDeriv_one
taylor_coeff_zero 📖	mathematical	—	coeff DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor eval	—	taylor_coeff hasseDeriv_zero LinearMap.id_apply
taylor_eq_zero 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor instZero	—	leadingCoeff_eq_zero leadingCoeff_taylor
taylor_eval 📖	mathematical	—	eval CommSemiring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	eval_comp eval_add eval_X eval_C
taylor_eval_sub 📖	mathematical	—	eval CommSemiring.toSemiring CommRing.toCommSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor	—	taylor_eval sub_add_cancel
taylor_inj 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor	—	taylor_injective
taylor_injective 📖	mathematical	—	Polynomial Ring.toSemiring DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor	—	injective_iff_map_eq_zero' DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass taylor_eq_zero
taylor_monomial 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor monomial instMul RingHom RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instAdd X	—	monomial_comp
taylor_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor instMul	—	mul_comp
taylor_one 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor instOne RingHom RingHom.instFunLike C AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	taylor_C
taylor_pow 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	RingHom.map_pow
taylor_taylor 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib	—	comp_assoc add_comp X_comp C_comp add_assoc map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
taylor_zero 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	taylor_apply C_0 add_zero comp_X
taylor_zero' 📖	mathematical	—	taylor MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring LinearMap.id Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid semiring module Semiring.toModule	—	LinearMap.ext taylor_zero
toAlgHom_taylorEquiv 📖	mathematical	—	AlgHomClass.toAlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semiring algebraOfAlgebra Algebra.id AlgEquiv AlgEquiv.instFunLike AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass taylorEquiv taylorAlgHom	—	AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass

---

← Back to Index