Documentation Verification Report

Polynomial

📁 Source: Mathlib/Topology/Algebra/Polynomial.lean

Statistics

Metric	Count
Definitions	0
Theorems `coeff_bdd_of_roots_le`, `coeff_le_of_roots_le`, `continuous`, `continuousAt`, `continuousAt_aeval`, `continuousOn`, `continuousOn_aeval`, `continuousWithinAt`, `continuousWithinAt_aeval`, `continuous_aeval`, `continuous_eval₂`, `eq_one_of_roots_le`, `exists_forall_norm_le`, `isClosedMap_eval`, `isProperMap_eval`, `tendsto_abv_aeval_atTop`, `tendsto_abv_atTop`, `tendsto_abv_eval₂_atTop`, `tendsto_norm_atTop`, `isClosedMap_pow`	20
Total	20

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coeff_bdd_of_roots_le` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `map` `natDegree` `Real` `Real.instLE` `Norm.norm` `NormedField.toNorm`	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `Real.instMax` `Real.instOne` `Real.instNatCast` `Nat.choose`	—	`instIsDomain` `le_or_gt` `LE.le.trans` `coeff_le_of_roots_le` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `Real.instIsOrderedRing` `pow_le_pow_left₀` `IsOrderedRing.toPosMulMono` `le_max_left` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `pow_le_pow_right₀` `le_max_right` `le_trans` `mul_le_mul_of_nonneg_left` `Nat.mono_cast` `Nat.choose_mono` `Nat.choose_le_middle` `le_of_lt` `pow_pos` `IsStrictOrderedRing.toPosMulStrictMono` `Real.instIsStrictOrderedRing` `IsStrictOrderedRing.toZeroLEOneClass` `lt_max_of_lt_right` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `eq_one_of_roots_le` `map_one` `coeff_one` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `instReflLe` `norm_zero` `one_le_mul_of_one_le_of_one_le` `one_le_pow₀` `IsStrictOrderedRing.toCharZero` `Nat.choose_pos`
`coeff_le_of_roots_le` 📖	mathematical	`Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `map` `Real` `Real.instLE` `Norm.norm` `NormedField.toNorm`	`Real` `Real.instLE` `Norm.norm` `NormedField.toNorm` `coeff` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `map` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.instMul` `Monoid.toPow` `Real.instMonoid` `natDegree` `Real.instNatCast` `Nat.choose`	—	`instIsDomain` `lt_or_ge` `eq_one_of_roots_le` `map_one` `natDegree_one` `zero_tsub` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `pow_zero` `one_mul` `coeff_one` `NormOneClass.norm_one` `NormedDivisionRing.to_normOneClass` `Nat.choose_self` `Nat.cast_one` `instReflLe` `norm_zero` `Real.instIsOrderedRing` `Monic.natDegree_map` `EuclideanDomain.toNontrivial` `coeff_eq_zero_of_natDegree_lt` `mul_nonneg` `IsOrderedRing.toPosMulMono` `pow_nonneg` `IsOrderedRing.toZeroLEOneClass` `Nat.cast_nonneg'` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `coeff_eq_esymm_roots_of_splits` `Monic.leadingCoeff` `Monic.map` `norm_mul` `NormedDivisionRing.toNormMulClass` `norm_pow` `norm_neg` `one_pow` `LE.le.trans` `norm_multiset_sum_le` `Multiset.sum_le_card_nsmul` `CanLift.prf` `NNReal.canLift` `coe_nnnorm` `NNReal.coe_pow` `NNReal.coe_le_coe` `nnnormHom_apply` `MonoidWithZeroHomClass.toMonoidHomClass` `MonoidWithZeroHom.monoidWithZeroHomClass` `MonoidHom.coe_coe` `MonoidHom.map_multiset_prod` `LE.le.trans_eq` `Multiset.prod_le_pow_card` `NNReal.mulLeftMono` `Multiset.mem_map` `Multiset.mem_of_le` `Multiset.mem_powersetCard` `Multiset.card_map` `Multiset.map_map` `Multiset.card_powersetCard` `Splits.natDegree_eq_card_roots` `Nat.choose_symm` `mul_comm` `nsmul_eq_mul` `le_refl`
`continuous` 📖	mathematical	—	`Continuous` `eval`	—	`continuous_eval₂`
`continuousAt` 📖	mathematical	—	`ContinuousAt` `eval`	—	`Continuous.continuousAt` `continuous`
`continuousAt_aeval` 📖	mathematical	—	`ContinuousAt` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval`	—	`Continuous.continuousAt` `continuous_aeval`
`continuousOn` 📖	mathematical	—	`ContinuousOn` `eval`	—	`Continuous.continuousOn` `continuous`
`continuousOn_aeval` 📖	mathematical	—	`ContinuousOn` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval`	—	`Continuous.continuousOn` `continuous_aeval`
`continuousWithinAt` 📖	mathematical	—	`ContinuousWithinAt` `eval`	—	`Continuous.continuousWithinAt` `continuous`
`continuousWithinAt_aeval` 📖	mathematical	—	`ContinuousWithinAt` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval`	—	`Continuous.continuousWithinAt` `continuous_aeval`
`continuous_aeval` 📖	mathematical	—	`Continuous` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval`	—	`continuous_eval₂`
`continuous_eval₂` 📖	mathematical	—	`Continuous` `eval₂`	—	`eval₂_eq_sum` `continuous_finset_sum` `IsSemitopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toIsSemitopologicalSemiring` `Continuous.mul` `IsTopologicalSemiring.toContinuousMul` `continuous_const` `continuous_pow`
`eq_one_of_roots_le` 📖	mathematical	`Real` `Real.instLT` `Real.instZero` `Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Splits` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NormedField.toField` `map` `Real.instLE` `Norm.norm` `NormedField.toNorm`	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instOne`	—	`instIsDomain` `Monic.natDegree_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₁` `Multiset.card_pos_iff_exists_mem` `zero_lt_iff` `Splits.natDegree_eq_card_roots` `Monic.natDegree_map` `EuclideanDomain.toNontrivial` `le_trans` `norm_nonneg`
`exists_forall_norm_le` 📖	mathematical	—	`Real` `Real.instLE` `Norm.norm` `NormedRing.toNorm` `eval` `Ring.toSemiring` `NormedRing.toRing`	—	`Continuous.exists_forall_le` `instClosedIicTopology` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `AddTorsor.nonempty` `Continuous.norm` `continuous` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `tendsto_norm_atTop` `tendsto_norm_cocompact_atTop` `eq_C_of_degree_le_zero` `le_of_not_gt` `coeff_C_zero` `eval_C` `instReflLe`
`isClosedMap_eval` 📖	mathematical	—	`IsClosedMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `eval` `Ring.toSemiring` `NormedRing.toRing`	—	`le_or_gt` `degree_le_zero_iff` `eval_C` `isClosedMap_const` `T2Space.t1Space` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `IsProperMap.isClosedMap` `isProperMap_eval`
`isProperMap_eval` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Ring.toSemiring` `NormedRing.toRing`	`IsProperMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `eval` `Ring.toSemiring` `NormedRing.toRing`	—	`isProperMap_iff_tendsto_cocompact` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `CompactlyCoherentSpace.of_sequentialSpace` `FrechetUrysohnSpace.to_sequentialSpace` `FirstCountableTopology.frechetUrysohnSpace` `TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology` `PseudoEMetricSpace.pseudoMetrizableSpace` `continuous` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalSeminormedRing.toIsTopologicalRing` `Metric.cobounded_eq_cocompact` `tendsto_norm_atTop_iff_cobounded` `tendsto_norm_atTop` `tendsto_norm_cobounded_atTop`
`tendsto_abv_aeval_atTop` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `CommSemiring.toSemiring` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.Tendsto` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `Ring.toSemiring` `algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `aeval` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tendsto_abv_eval₂_atTop`
`tendsto_abv_atTop` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Ring.toSemiring` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.Tendsto` `eval` `Ring.toSemiring` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`tendsto_abv_eval₂_atTop` `leadingCoeff_eq_zero` `ne_zero_of_degree_gt`
`tendsto_abv_eval₂_atTop` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Filter.Tendsto` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	`Filter.Tendsto` `eval₂` `Ring.toSemiring` `Filter.atTop` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder`	—	`degree_pos_induction_on` `eval₂_mul_X` `eval₂_C` `IsAbsoluteValue.abv_mul` `Filter.Tendsto.const_mul_atTop` `IsAbsoluteValue.abv_pos` `leadingCoeff_C` `leadingCoeff_mul_X` `Filter.Tendsto.atTop_mul_atTop₀` `IsStrictOrderedRing.toIsOrderedRing` `Filter.Tendsto.atTop_of_add_const` `IsStrictOrderedRing.toIsOrderedCancelAddMonoid` `Filter.tendsto_atTop_mono` `IsAbsoluteValue.abv_add` `eval₂_add` `add_neg_cancel_right` `leadingCoeff_add_of_degree_lt` `LE.le.trans_lt` `degree_C_le` `add_comm`
`tendsto_norm_atTop` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `degree` `Ring.toSemiring` `NormedRing.toRing` `Filter.Tendsto` `Real` `Norm.norm` `NormedRing.toNorm` `Filter.atTop` `Real.instPreorder`	`Filter.Tendsto` `Real` `Norm.norm` `NormedRing.toNorm` `eval` `Ring.toSemiring` `NormedRing.toRing` `Filter.atTop` `Real.instPreorder`	—	`tendsto_abv_atTop` `Real.instIsStrictOrderedRing`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isClosedMap_pow` 📖	mathematical	—	`IsClosedMap` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedRing.toPseudoMetricSpace` `NormedRing.toSeminormedRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `NormedRing.toRing`	—	`Polynomial.eval_X_pow` `Polynomial.isClosedMap_eval`

---

← Back to Index