DualNumber

📁 Source: Mathlib/Analysis/Normed/Algebra/DualNumber.lean

Statistics

Metric	Count
Definitions	0
Theorems exp_eps, exp_smul_eps	2
Total	2

DualNumber

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exp_eps 📖	mathematical	—	NormedSpace.exp DualNumber TrivSqZeroExt.ring CommRing.toRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsScalarTower.right CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id TrivSqZeroExt.instTopologicalSpace UniformSpace.toTopologicalSpace TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite IsTopologicalRing.to_topologicalAddGroup NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring ContinuousMul.to_continuousSMul_op eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne TrivSqZeroExt.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib TrivSqZeroExt.one	—	TrivSqZeroExt.exp_inr SMulCommClass.opposite_mid IsScalarTower.right IsTopologicalRing.to_topologicalAddGroup ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ContinuousMul.to_continuousSMul_op
exp_smul_eps 📖	mathematical	—	NormedSpace.exp DualNumber TrivSqZeroExt.ring CommRing.toRing Ring.toAddCommGroup Semiring.toModule Ring.toSemiring Semiring.toOppositeModule SMulCommClass.opposite_mid MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Module.toDistribMulAction AddCommGroup.toAddCommMonoid IsScalarTower.right CommRing.toCommSemiring CommSemiring.toSemiring Algebra.id TrivSqZeroExt.instTopologicalSpace UniformSpace.toTopologicalSpace TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite IsTopologicalRing.to_topologicalAddGroup NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring IsTopologicalRing.toIsTopologicalSemiring ContinuousMul.to_continuousSMul_op TrivSqZeroExt.smul Algebra.toSMul eps MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne TrivSqZeroExt.add Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib TrivSqZeroExt.one	—	SMulCommClass.opposite_mid IsScalarTower.right TrivSqZeroExt.instIsTopologicalRingOfIsTopologicalAddGroupOfContinuousSMulMulOpposite IsTopologicalRing.to_topologicalAddGroup ContinuousMul.to_continuousSMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring ContinuousMul.to_continuousSMul_op eps.eq_1 TrivSqZeroExt.inr_smul TrivSqZeroExt.exp_inr

---

← Back to Index