Documentation Verification Report

CPolynomial

📁 Source: Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems `contDiffAt`, `contDiffOn`, `contDiff`, `contDiffAt`	4
Total	4

CPolynomialAt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffAt` 📖	mathematical	`CPolynomialAt`	`ContDiffAt`	—	`exists_mem_nhds_cpolynomialOn` `ContDiffOn.contDiffAt` `CPolynomialOn.contDiffOn`

CPolynomialOn

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiffOn` 📖	mathematical	`CPolynomialOn`	`ContDiffOn`	—	`analyticOnNhd` `isOpen_cpolynomialAt` `AnalyticOnNhd.contDiffOn` `IsOpen.uniqueDiffOn` `NormedField.nhdsNE_neBot` `IsBoundedSMul.continuousSMul` `NormedSpace.toIsBoundedSMul` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `ContDiffOn.mono`

ContinuousMultilinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`contDiff` 📖	mathematical	—	`ContDiff` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike`	—	`contDiff_iff_contDiffAt` `contDiffAt`
`contDiffAt` 📖	mathematical	—	`ContDiffAt` `Pi.normedAddCommGroup` `Pi.normedSpace` `NontriviallyNormedField.toNormedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `DFunLike.coe` `ContinuousMultilinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `funLike`	—	`CPolynomialAt.contDiffAt` `cpolynomialAt`

---

← Back to Index