Polynomial

📁 Source: Mathlib/Analysis/Analytic/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems aeval_mvPolynomial, aeval_polynomial, aeval_polynomial, eval_polynomial, aeval_mvPolynomial, aeval_polynomial, eval_continuousLinearMap, eval_continuousLinearMap', eval_linearMap, eval_linearMap', eval_mvPolynomial, eval_polynomial, aeval_polynomial	13
Total	13

AnalyticAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_mvPolynomial 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring NormedCommRing.toCommRing MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval	—	MvPolynomial.induction_on MvPolynomial.aeval_C analyticAt_const map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass add map_mul NonUnitalAlgSemiHomClass.toMulHomClass MvPolynomial.aeval_X mul
aeval_polynomial 📖	mathematical	AnalyticAt NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Ring.toSemiring NormedRing.toRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	analyticWithinAt_univ AnalyticWithinAt.aeval_polynomial

AnalyticOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_polynomial 📖	mathematical	AnalyticOn NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Ring.toSemiring NormedRing.toRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	AnalyticWithinAt.aeval_polynomial
eval_polynomial 📖	mathematical	—	AnalyticOn NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Set.univ	—	aeval_polynomial analyticOn_id

AnalyticOnNhd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_mvPolynomial 📖	mathematical	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing	DFunLike.coe AlgHom MvPolynomial CommSemiring.toSemiring MvPolynomial.commSemiring CommRing.toCommSemiring NormedCommRing.toCommRing MvPolynomial.algebra Algebra.id AlgHom.funLike MvPolynomial.aeval	—	AnalyticAt.aeval_mvPolynomial
aeval_polynomial 📖	mathematical	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Ring.toSemiring NormedRing.toRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	AnalyticAt.aeval_polynomial
eval_continuousLinearMap 📖	mathematical	—	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring NormedCommRing.toCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.topologicalSpace SeminormedRing.toPseudoMetricSpace Pi.addCommMonoid NormedSpace.toModule Pi.Function.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousLinearMap.funLike Set.univ	—	AnalyticAt.aeval_mvPolynomial RingHomCompTriple.ids ContinuousLinearMap.analyticAt
eval_continuousLinearMap' 📖	mathematical	—	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring NormedCommRing.toCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval ContinuousLinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing ContinuousLinearMap.funLike Set.univ	—	AnalyticAt.aeval_mvPolynomial ContinuousLinearMap.analyticAt
eval_linearMap 📖	mathematical	—	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring NormedCommRing.toCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid Pi.addCommMonoid SeminormedRing.toPseudoMetricSpace NormedSpace.toModule Pi.Function.module NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike Set.univ	—	eval_continuousLinearMap LinearMap.continuous_of_finiteDimensional SeminormedAddCommGroup.toIsTopologicalAddGroup IsBoundedSMul.continuousSMul NormedSpace.toIsBoundedSMul Pi.topologicalAddGroup instContinuousSMulForall
eval_linearMap' 📖	mathematical	—	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing DFunLike.coe RingHom MvPolynomial CommRing.toCommSemiring NormedCommRing.toCommRing Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField RingHom.id ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid SeminormedRing.toPseudoMetricSpace NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing LinearMap.instFunLike Set.univ	—	eval_linearMap
eval_mvPolynomial 📖	mathematical	—	AnalyticOnNhd Pi.normedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField Pi.normedSpace NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace DFunLike.coe RingHom MvPolynomial Semifield.toCommSemiring Field.toSemifield NormedField.toField Semiring.toNonAssocSemiring CommSemiring.toSemiring MvPolynomial.commSemiring RingHom.instFunLike MvPolynomial.eval Set.univ	—	eval_linearMap Pi.t2Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace FiniteDimensional.finiteDimensional_pi' Finite.of_fintype FiniteDimensional.finiteDimensional_self
eval_polynomial 📖	mathematical	—	AnalyticOnNhd NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing Polynomial.eval CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing Set.univ	—	aeval_polynomial analyticOnNhd_id

AnalyticWithinAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
aeval_polynomial 📖	mathematical	AnalyticWithinAt NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing NormedAlgebra.toNormedSpace NontriviallyNormedField.toNormedField NormedRing.toSeminormedRing	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring Polynomial.semiring Ring.toSemiring NormedRing.toRing Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	Polynomial.induction_on Polynomial.aeval_C analyticWithinAt_const Polynomial.aeval_add add pow_succ Polynomial.aeval_mul Polynomial.aeval_X mul

---

← Back to Index