Documentation Verification Report

Polynomial

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

Statistics

Metric	Count
Definitions `toContinuousMap`, `toContinuousMapAlgHom`, `toContinuousMapOn`, `toContinuousMapOnAlgHom`, `polynomialFunctions`	5
Theorems `aeval_continuousMap_apply`, `toContinuousMapAlgHom_apply`, `toContinuousMapOnAlgHom_apply`, `toContinuousMapOn_X_eq_restrict_id`, `toContinuousMapOn_apply`, `toContinuousMap_X_eq_id`, `toContinuousMap_apply`, `comap_compRightAlgHom_iccHomeoI`, `eq_adjoin_X`, `le_equalizer`, `starClosure_eq_adjoin_X`, `starClosure_le_equalizer`, `polynomialFunctions_coe`, `polynomialFunctions_separatesPoints`	14
Total	19

Polynomial

Definitions

Name	Category	Theorems
`toContinuousMap` 📖	CompOp	4 math math: `toContinuousMap_apply`, `toContinuousMap_X_eq_id`, `toContinuousMapAlgHom_apply`, `toContinuousMapOn_apply`
`toContinuousMapAlgHom` 📖	CompOp	1 math math: `toContinuousMapAlgHom_apply`
`toContinuousMapOn` 📖	CompOp	6 math math: `toContinuousMapOn_X_eq_restrict_id`, `exists_polynomial_near_continuousMap`, `ContinuousMap.polynomial_comp_attachBound`, `ContinuousMap.polynomial_comp_attachBound_mem`, `toContinuousMapOn_apply`, `toContinuousMapOnAlgHom_apply`
`toContinuousMapOnAlgHom` 📖	CompOp	4 math math: `polynomialFunctions.eq_adjoin_X`, `polynomialFunctions.starClosure_eq_adjoin_X`, `polynomialFunctions_coe`, `toContinuousMapOnAlgHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_continuousMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `aeval` `eval`	—	`induction_on'` `IsTopologicalSemiring.toContinuousAdd` `map_add` `SemilinearMapClass.toAddHomClass` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `eval_add` `aeval_monomial` `algebraMap_apply` `mul_one` `eval_monomial`
`toContinuousMapAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `ContinuousMap` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toContinuousMapAlgHom` `toContinuousMap`	—	—
`toContinuousMapOnAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `semiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `algebraOfAlgebra` `Algebra.id` `ContinuousMap.algebra` `AlgHom.funLike` `toContinuousMapOnAlgHom` `toContinuousMapOn`	—	—
`toContinuousMapOn_X_eq_restrict_id` 📖	mathematical	—	`toContinuousMapOn` `X` `ContinuousMap.restrict` `ContinuousMap.id`	—	`ContinuousMap.ext` `eval_X`
`toContinuousMapOn_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instFunLike` `toContinuousMapOn` `toContinuousMap`	—	—
`toContinuousMap_X_eq_id` 📖	mathematical	—	`toContinuousMap` `X` `ContinuousMap.id`	—	`ContinuousMap.ext` `eval_X`
`toContinuousMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `toContinuousMap` `eval`	—	—

(root)

Definitions

Name	Category	Theorems
`polynomialFunctions` 📖	CompOp	12 math math: `polynomialFunctions.eq_adjoin_X`, `polynomialFunctions.le_equalizer`, `polynomialFunctions_separatesPoints`, `polynomialFunctions.starClosure_topologicalClosure`, `polynomialFunctions.starClosure_le_equalizer`, `continuousMap_mem_polynomialFunctions_closure`, `polynomialFunctions.starClosure_eq_adjoin_X`, `polynomialFunctions_coe`, `polynomialFunctions.topologicalClosure`, `polynomialFunctions_closure_eq_top'`, `polynomialFunctions_closure_eq_top`, `polynomialFunctions.comap_compRightAlgHom_iccHomeoI`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`polynomialFunctions_coe` 📖	mathematical	—	`SetLike.coe` `Subalgebra` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `ContinuousMap.algebra` `Algebra.id` `Subalgebra.instSetLike` `polynomialFunctions` `Set.range` `Polynomial` `DFunLike.coe` `AlgHom` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.toContinuousMapOnAlgHom`	—	`Set.ext` `Algebra.map_top`
`polynomialFunctions_separatesPoints` 📖	mathematical	—	`Subalgebra.SeparatesPoints` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `CommSemiring.toSemiring` `Algebra.id` `polynomialFunctions`	—	`Algebra.mem_top` `Polynomial.eval_X`

polynomialFunctions

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_compRightAlgHom_iccHomeoI` 📖	mathematical	`Real` `Real.instLT`	`Subalgebra.comap` `ContinuousMap` `Set.Elem` `Set.Icc` `Real.instPreorder` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `unitInterval` `Real.instCommSemiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `Real.semiring` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `NonUnitalNormedCommRing.toNonUnitalCommRing` `NormedCommRing.toNonUnitalNormedCommRing` `Real.normedCommRing` `instIsTopologicalRingReal` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.compRightAlgHom` `toContinuousMap` `Homeomorph` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.linearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `CommRing.toNonUnitalCommRing` `Field.toCommRing` `Real.instField` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `EquivLike.toFunLike` `Homeomorph.instEquivLike` `Homeomorph.instContinuousMapClass` `Homeomorph.symm` `iccHomeoI` `Real.instIsStrictOrderedRing` `polynomialFunctions`	—	`Subalgebra.ext` `IsTopologicalRing.toIsTopologicalSemiring` `instIsTopologicalRingReal` `Homeomorph.instContinuousMapClass` `Real.instIsStrictOrderedRing` `ContinuousMap.ext` `neg_mul` `map_neg` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Polynomial.eval_comp` `Polynomial.eval_add` `Polynomial.eval_smul` `IsScalarTower.right` `Polynomial.eval_X` `Polynomial.eval_neg` `Polynomial.eval_mul` `Polynomial.eval_C` `mul_comm` `add_mul` `Distrib.rightDistribClass` `sub_eq_add_neg` `inv_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `sub_pos` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `sub_nonneg` `sub_le_sub_right` `mul_nonneg` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_of_lt` `div_eq_mul_inv` `div_le_one` `sub_ne_zero_of_ne` `LT.lt.ne` `Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq` `IsCancelMulZero.toIsLeftCancelMulZero` `instIsCancelMulZero` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `one_mul` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `div_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.subst_sub` `Mathlib.Tactic.FieldSimp.NF.inv_eq_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `mul_one` `mul_neg` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `one_ne_zero` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.atom_pf` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.neg_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.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Meta.NormNum.IsInt.to_isNat` `Mathlib.Meta.NormNum.isInt_add` `DFunLike.ext_iff`
`eq_adjoin_X` 📖	mathematical	—	`polynomialFunctions` `Algebra.adjoin` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `ContinuousMap.algebra` `Algebra.id` `Set.instSingletonSet` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.toContinuousMapOnAlgHom` `Polynomial.X`	—	`le_antisymm` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `AlgHom.coe_toRingHom` `Polynomial.induction_on` `Polynomial.C_eq_algebraMap` `AlgHomClass.commutes` `Subalgebra.algebraMap_mem` `IsTopologicalSemiring.toContinuousAdd` `map_add` `SemilinearMapClass.toAddHomClass` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass` `IsTopologicalSemiring.toContinuousMul` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AddMemClass.add_mem` `AddSubmonoidClass.toAddMemClass` `SubsemiringClass.toAddSubmonoidClass` `Subalgebra.instSubsemiringClass` `pow_succ` `mul_assoc` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MulMemClass.mul_mem` `SubmonoidClass.toMulMemClass` `SubsemiringClass.toSubmonoidClass` `Algebra.subset_adjoin` `Set.mem_singleton` `Algebra.adjoin_le` `Set.mem_singleton_iff`
`le_equalizer` 📖	mathematical	`DFunLike.coe` `AlgHom` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `ContinuousMap.algebra` `Algebra.id` `AlgHom.funLike` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Polynomial.toContinuousMapOnAlgHom` `Polynomial.X`	`Subalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `Subalgebra.instPartialOrder` `polynomialFunctions` `AlgHom.equalizer` `AlgHom.algHomClass`	—	`AlgHom.algHomClass` `eq_adjoin_X` `AlgHom.adjoin_le_equalizer` `Set.mem_singleton_iff`
`starClosure_eq_adjoin_X` 📖	mathematical	—	`Subalgebra.starClosure` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStarRingOfContinuousStar` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `ContinuousMap.instStarModule` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `Algebra.toSMul` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `polynomialFunctions` `StarAlgebra.adjoin` `Set.instSingletonSet` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.toContinuousMapOnAlgHom` `Polynomial.X`	—	`ContinuousMap.instStarModule` `StarMul.toStarModule` `eq_adjoin_X` `StarAlgebra.adjoin_eq_starClosure_adjoin`
`starClosure_le_equalizer` 📖	mathematical	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `ContinuousMap.algebra` `Algebra.id` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `AlgHom` `Polynomial` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `AlgHom.funLike` `Polynomial.toContinuousMapOnAlgHom` `Polynomial.X`	`StarSubalgebra` `ContinuousMap.instStarRingOfContinuousStar` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `ContinuousMap.instStarModule` `Algebra.toSMul` `StarMul.toStarModule` `CommSemiring.toCommMonoid` `StarRing.toStarMul` `Preorder.toLE` `PartialOrder.toPreorder` `StarSubalgebra.instPartialOrder` `Subalgebra.starClosure` `polynomialFunctions` `StarAlgHom.equalizer` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass`	—	`ContinuousMap.instStarModule` `StarMul.toStarModule` `StarAlgHom.instAlgHomClass` `StarAlgHom.instStarHomClass` `starClosure_eq_adjoin_X` `StarAlgHom.adjoin_le_equalizer` `Set.mem_singleton_iff`

---

← Back to Index