Documentation Verification Report

AnalyticalPart

📁 Source: Mathlib/NumberTheory/Transcendental/Lindemann/AnalyticalPart.lean

Statistics

Metric	Count
Definitions	0
Theorems `exp_polynomial_approx`, `hasDerivAt_cexp_mul_sumIDeriv`, `integral_exp_mul_eval`	3
Total	3

LindemannWeierstrass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exp_polynomial_approx` 📖	mathematical	—	`Polynomial.natDegree` `Int.instSemiring` `Real` `Real.instLE` `Norm.norm` `Complex` `Complex.instNorm` `Complex.instSub` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `NormedAddGroup.toAddGroup` `NormedAddCommGroup.toNormedAddGroup` `Complex.instNormedAddCommGroup` `Complex.exp` `AddMonoid.toNatSMul` `ESeminormedAddMonoid.toAddMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Int.instCommSemiring` `Polynomial.semiring` `Complex.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Ring.toIntAlgebra` `Complex.instRing` `AlgHom.funLike` `Polynomial.aeval` `DivInvMonoid.toDiv` `Real.instDivInvMonoid` `Monoid.toNatPow` `Real.instMonoid` `Real.instNatCast` `Nat.factorial`	—	`instIsDomain` `nsmul_eq_mul` `zsmul_eq_mul` `Polynomial.eval_sumIDeriv_of_pos` `Int.instNontrivial` `NormMulClass.toNoZeroDivisors` `Int.instNormMulClass` `Nat.Prime.pos` `dvd_add_left` `dvd_mul_right` `Mathlib.Tactic.Contrapose.contrapose₃` `Int.natCast_dvd` `Int.Prime.dvd_pow'` `Polynomial.aeval_sumIDeriv` `LE.le.trans` `tsub_le_tsub_right` `Nat.instOrderedSub` `Polynomial.natDegree_mul_le` `Polynomial.natDegree_X_pow` `Polynomial.natDegree_pow` `tsub_add_eq_add_tsub` `StarOrderedRing.toExistsAddOfLE` `Nat.instStarOrderedRing` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Nat.Prime.one_le` `tsub_right_comm` `add_tsub_cancel_left` `le_refl` `Int.cast_add` `Int.cast_pow` `Int.cast_mul` `Int.cast_natCast` `Nat.cast_mul` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.mul_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.pow_congr` `Mathlib.Tactic.Ring.atom_pf` `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.add_pf_add_zero` `Mathlib.Tactic.Ring.zero_mul` `Mathlib.Tactic.Ring.add_pf_add_lt` `Mathlib.Tactic.Ring.add_pf_zero_add` `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.mul_one` `le_div_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `Real.instIsStrictOrderedRing` `Nat.cast_pos` `Real.instIsOrderedRing` `Real.instNontrivial` `Nat.factorial_pos` `Complex.norm_natCast` `norm_mul` `NormedDivisionRing.toNormMulClass` `Nat.mul_factorial_pred` `Nat.Prime.ne_zero` `mul_sub` `Polynomial.map_mul` `Polynomial.map_pow` `dvd_mul_of_dvd_right` `pow_dvd_pow_of_dvd` `Polynomial.dvd_iff_isRoot` `Polynomial.mem_roots'` `Polynomial.eval_pow` `Polynomial.C_0` `sub_zero` `mul_comm` `eq_intCast` `RingHom.instRingHomClass` `Polynomial.aeval_algebraMap_apply_eq_algebraMap_eval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `Polynomial.aeval_sumIDeriv_eq_eval` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `IsOrderedRing.toMulPosMono` `Multiset.mem_map_of_mem` `Finset.le_max'`
`hasDerivAt_cexp_mul_sumIDeriv` 📖	mathematical	—	`HasDerivAt` `Real` `DenselyNormedField.toNontriviallyNormedField` `Real.denselyNormedField` `Complex` `Complex.addCommGroup` `NormedSpace.toModule` `Real.normedField` `NonUnitalSeminormedRing.toSeminormedAddCommGroup` `NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing` `SeminormedCommRing.toNonUnitalSeminormedCommRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `InnerProductSpace.toNormedSpace` `Real.instRCLike` `instInnerProductSpaceRealComplex` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `SeminormedCommRing.toSeminormedRing` `IsBoundedSMul.continuousSMul` `Real.pseudoMetricSpace` `Real.instZero` `Complex.instZero` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `NontriviallyNormedField.toNormedField` `Module.toDistribMulAction` `AddCommGroup.toAddCommMonoid` `NormedSpace.toIsBoundedSMul` `Complex.instNeg` `Complex.instMul` `Complex.exp` `Algebra.toSMul` `Semifield.toCommSemiring` `Ring.toSemiring` `SeminormedRing.toRing` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `Polynomial.eval` `Complex.instSemiring` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.sumIDeriv`	—	`IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `HasDerivAt.smul_const` `IsScalarTower.left` `hasDerivAt_id'` `HasDerivAt.cexp` `HasDerivAt.fun_neg` `HasDerivAt.comp` `Polynomial.hasDerivAt` `Polynomial.sumIDeriv_eq_self_add` `one_smul` `Polynomial.eval_add` `Mathlib.Tactic.Ring.of_eq` `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.neg_congr` `Mathlib.Tactic.Ring.add_congr` `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.mul_one` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `Mathlib.Meta.NormNum.IsNat.to_raw_eq` `HasDerivAt.mul`
`integral_exp_mul_eval` 📖	mathematical	—	`Complex` `Complex.instMul` `intervalIntegral` `Complex.instNormedAddCommGroup` `InnerProductSpace.toNormedSpace` `Real` `Real.instRCLike` `NormedAddCommGroup.toSeminormedAddCommGroup` `instInnerProductSpaceRealComplex` `Complex.exp` `Complex.instNeg` `Algebra.toSMul` `Semifield.toCommSemiring` `Field.toSemifield` `NormedField.toField` `Real.normedField` `Ring.toSemiring` `SeminormedRing.toRing` `SeminormedCommRing.toSeminormedRing` `NormedCommRing.toSeminormedCommRing` `NormedField.toNormedCommRing` `Complex.instNormedField` `NormedAlgebra.toAlgebra` `RCLike.toNormedAlgebra` `Complex.instRCLike` `Polynomial.eval` `Complex.instSemiring` `Real.instZero` `Real.instOne` `MeasureTheory.MeasureSpace.volume` `Real.measureSpace` `Complex.instAdd` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Polynomial` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Polynomial.semiring` `Polynomial.module` `Semiring.toModule` `LinearMap.instFunLike` `Polynomial.sumIDeriv` `Complex.instZero`	—	`intervalIntegral.integral_const_mul` `intervalIntegral.integral_eq_sub_of_hasDerivAt` `Complex.instCompleteSpace` `hasDerivAt_cexp_mul_sumIDeriv` `ContinuousOn.intervalIntegrable` `Real.locallyFinite_volume` `ContinuousOn.fun_mul` `IsTopologicalSemiring.toContinuousMul` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalDivisionRing.toIsTopologicalRing` `NormedDivisionRing.to_isTopologicalDivisionRing` `continuousOn_const` `ContinuousOn.cexp` `ContinuousOn.neg` `IsTopologicalRing.toContinuousNeg` `ContinuousOn.smul` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `continuousOn_id'` `Continuous.comp_continuousOn'` `Polynomial.continuous` `one_smul` `zero_smul` `neg_zero` `Complex.exp_zero` `one_mul` `sub_neg_eq_add`

---

← Back to Index