Polynomial

📁 Source: Mathlib/Analysis/Calculus/Deriv/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems deriv, derivWithin, derivWithin_aeval, deriv_aeval, differentiable, differentiableAt, differentiableAt_aeval, differentiableOn, differentiableOn_aeval, differentiableWithinAt, differentiableWithinAt_aeval, differentiable_aeval, fderiv, fderivWithin, fderivWithin_aeval, fderiv_aeval, hasDerivAt, hasDerivAt_aeval, hasDerivWithinAt, hasDerivWithinAt_aeval, hasFDerivAt, hasFDerivAt_aeval, hasFDerivWithinAt, hasFDerivWithinAt_aeval, hasStrictDerivAt, hasStrictDerivAt_aeval	26
Total	26

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
deriv 📖	mathematical	—	deriv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasDerivAt.deriv hasDerivAt
derivWithin 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	derivWithin eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	DifferentiableAt.derivWithin differentiableAt deriv
derivWithin_aeval 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	derivWithin DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	eval₂_eq_eval_map derivative_map derivWithin
deriv_aeval 📖	mathematical	—	deriv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasDerivAt.deriv hasDerivAt_aeval
differentiable 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	differentiableAt
differentiableAt 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	HasDerivAt.differentiableAt hasDerivAt
differentiableAt_aeval 📖	mathematical	—	DifferentiableAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	HasDerivAt.differentiableAt hasDerivAt_aeval
differentiableOn 📖	mathematical	—	DifferentiableOn NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	Differentiable.differentiableOn differentiable
differentiableOn_aeval 📖	mathematical	—	DifferentiableOn NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	Differentiable.differentiableOn differentiable_aeval
differentiableWithinAt 📖	mathematical	—	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField	—	DifferentiableAt.differentiableWithinAt differentiableAt
differentiableWithinAt_aeval 📖	mathematical	—	DifferentiableWithinAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	DifferentiableAt.differentiableWithinAt differentiableAt_aeval
differentiable_aeval 📖	mathematical	—	Differentiable NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval	—	differentiableAt_aeval
fderiv 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap.smulRight ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsScalarTower.right Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.one DFunLike.coe LinearMap Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasFDerivAt.fderiv IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt
fderivWithin 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	fderivWithin eval ContinuousLinearMap.smulRight ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsScalarTower.right Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.one DFunLike.coe LinearMap Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasFDerivWithinAt.fderivWithin IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivWithinAt
fderivWithin_aeval 📖	mathematical	UniqueDiffWithinAt DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField NontriviallyNormedField.toNormedField NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing	fderivWithin DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval ContinuousLinearMap.smulRight ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsScalarTower.right Semifield.toCommSemiring ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.one LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasFDerivWithinAt.fderivWithin IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivWithinAt_aeval
fderiv_aeval 📖	mathematical	—	fderiv NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval ContinuousLinearMap.smulRight ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid IsScalarTower.right Semifield.toCommSemiring ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ContinuousLinearMap.one LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasFDerivAt.fderiv IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing IsTopologicalSemiring.toContinuousAdd TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace hasFDerivAt_aeval
hasDerivAt 📖	mathematical	—	HasDerivAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasStrictDerivAt.hasDerivAt hasStrictDerivAt
hasDerivAt_aeval 📖	mathematical	—	HasDerivAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasStrictDerivAt.hasDerivAt hasStrictDerivAt_aeval
hasDerivWithinAt 📖	mathematical	—	HasDerivWithinAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasDerivAt.hasDerivWithinAt hasDerivAt
hasDerivWithinAt_aeval 📖	mathematical	—	HasDerivWithinAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasDerivAt.hasDerivWithinAt hasDerivAt_aeval
hasFDerivAt 📖	mathematical	—	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap.smulRight AddCommGroup.toAddCommMonoid IsScalarTower.right Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.one DFunLike.coe LinearMap Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	hasDerivAt
hasFDerivAt_aeval 📖	mathematical	—	HasFDerivAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval ContinuousLinearMap.smulRight AddCommGroup.toAddCommMonoid IsScalarTower.right Semifield.toCommSemiring ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.one LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	hasDerivAt_aeval
hasFDerivWithinAt 📖	mathematical	—	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing eval DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField ContinuousLinearMap.smulRight AddCommGroup.toAddCommMonoid IsScalarTower.right Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.one DFunLike.coe LinearMap Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasFDerivAt.hasFDerivWithinAt IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasFDerivAt
hasFDerivWithinAt_aeval 📖	mathematical	—	HasFDerivWithinAt SeminormedAddCommGroup.toAddCommGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField algebraOfAlgebra Algebra.id AlgHom.funLike aeval ContinuousLinearMap.smulRight AddCommGroup.toAddCommMonoid IsScalarTower.right Semifield.toCommSemiring ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring ESeminormedAddCommMonoid.toAddCommMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid ContinuousLinearMap.one LinearMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	HasFDerivAt.hasFDerivWithinAt IsScalarTower.right ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing hasFDerivAt_aeval
hasStrictDerivAt 📖	mathematical	—	HasStrictDerivAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing eval DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative	—	induction_on' ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasStrictDerivAt.congr_simp eval_add derivative_add HasStrictDerivAt.add eval_monomial derivative_monomial mul_assoc HasStrictDerivAt.const_mul hasStrictDerivAt_pow
hasStrictDerivAt_aeval 📖	mathematical	—	HasStrictDerivAt NormedAddCommGroup.toAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing NontriviallyNormedField.toNormedField NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing ContinuousMul.to_continuousSMul MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule LinearMap.instFunLike derivative	—	ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing HasStrictDerivAt.congr_simp eval₂_eq_eval_map derivative_map hasStrictDerivAt

---

← Back to Index