Algebra

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

Statistics

Metric	Count
Definitions `compLeftContinuous`, `compLeftContinuous`, `instCoeFunElemForallSetOfContinuous`, `compLeftContinuous`, `const`, `C`, `algebra`, `coeFnAddMonoidHom`, `coeFnAlgHom`, `coeFnLinearMap`, `coeFnMonoidHom`, `coeFnRingHom`, `compAddMonoidHom'`, `compMonoidHom'`, `compRightAlgHom`, `evalAlgHom`, `evalCLM`, `instAdd`, `instAddCommGroupContinuousMap`, `instAddCommMonoidOfContinuousAdd`, `instAddCommSemigroupOfContinuousAdd`, `instAddGroupOfIsTopologicalAddGroup`, `instAddMonoidOfContinuousAdd`, `instAddMonoidWithOneOfContinuousAdd`, `instAddSemigroupOfContinuousAdd`, `instAddZeroClassOfContinuousAdd`, `instCommGroupContinuousMap`, `instCommMonoidOfContinuousMul`, `instCommMonoidWithZeroOfContinuousMul`, `instCommRingOfIsTopologicalRing`, `instCommSemigroupOfContinuousMul`, `instCommSemiringOfIsTopologicalSemiring`, `instDistribMulActionOfContinuousConstSMul`, `instDivOfContinuousDiv`, `instGroupOfIsTopologicalGroup`, `instIntCast`, `instInvOfContinuousInv`, `instMonoidOfContinuousMul`, `instMonoidWithZeroOfContinuousMul`, `instMul`, `instMulActionOfContinuousConstSMul`, `instMulOneClassOfContinuousMul`, `instMulZeroClassOfContinuousMul`, `instNSMul`, `instNatCast`, `instNegOfContinuousNeg`, `instNonAssocRingOfIsTopologicalRing`, `instNonAssocSemiringOfIsTopologicalSemiring`, `instNonUnitalCommRingOfIsTopologicalRing`, `instNonUnitalCommSemiringOfIsTopologicalSemiring`, `instNonUnitalNonAssocRingOfIsTopologicalRing`, `instNonUnitalNonAssocSemiringOfIsTopologicalSemiring`, `instNonUnitalRingOfIsTopologicalRing`, `instNonUnitalSemiringOfIsTopologicalSemiring`, `instOne`, `instPow`, `instRing`, `instSMul`, `instSMul'`, `instSemigroupOfContinuousMul`, `instSemigroupWithZeroOfContinuousMul`, `instSemiringOfIsTopologicalSemiring`, `instSubOfContinuousSub`, `instVAdd`, `instZPow`, `instZSMul`, `instZero`, `module'`, `compLeftContinuous`, `compLeftContinuous`, `SeparatesPointsStrongly`, `SeparatesPoints`, `continuousAddSubgroup`, `continuousAddSubmonoid`, `continuousSubalgebra`, `continuousSubgroup`, `continuousSubmodule`, `continuousSubmonoid`, `continuousSubring`, `continuousSubsemiring`	80
Theorems `compLeftContinuous_apply`, `compLeftContinuous_apply_apply`, `compLeftContinuous_apply`, `const_apply_apply`, `C_apply`, `add_apply`, `add_comp`, `coeFnAddMonoidHom_apply`, `coeFnAlgHom_apply`, `coeFnLinearMap_apply`, `coeFnMonoidHom_apply`, `coeFnRingHom_apply`, `coe_add`, `coe_div`, `coe_intCast`, `coe_inv`, `coe_mul`, `coe_natCast`, `coe_neg`, `coe_nsmul`, `coe_one`, `coe_pow`, `coe_prod`, `coe_smul`, `coe_smul'`, `coe_sub`, `coe_sum`, `coe_vadd`, `coe_zero`, `coe_zpow`, `coe_zsmul`, `compAddMonoidHom'_apply`, `compMonoidHom'_apply`, `compRightAlgHom_apply`, `compRightAlgHom_continuous`, `comp_one`, `comp_zero`, `const_one`, `const_zero`, `div_apply`, `div_comp`, `evalAlgHom_apply`, `evalCLM_apply`, `hasProd_apply`, `hasSum_apply`, `instContinuousAddOfLocallyCompactSpace`, `instContinuousConstSMul`, `instContinuousConstVAdd`, `instContinuousMulOfLocallyCompactSpace`, `instContinuousSMul`, `instContinuousVAdd`, `instIsCentralScalar`, `instIsScalarTower`, `instIsScalarTower_1`, `instIsTopologicalAddGroup`, `instIsTopologicalGroup`, `instIsTopologicalRingOfLocallyCompactSpace`, `instIsTopologicalSemiringOfLocallyCompactSpace`, `instSMulCommClass`, `instSMulCommClass_1`, `instSMulCommClass_2`, `instVAddCommClass`, `intCast_apply`, `inv_apply`, `inv_comp`, `mul_apply`, `mul_comp`, `multipliable_apply`, `natCast_apply`, `neg_apply`, `neg_comp`, `nsmul_apply`, `nsmul_comp`, `one_apply`, `one_comp`, `pow_apply`, `pow_comp`, `prod_apply`, `smul_apply`, `smul_apply'`, `smul_comp`, `sub_apply`, `sub_comp`, `subsingleton_subalgebra`, `sum_apply`, `summable_apply`, `tprod_apply`, `tsum_apply`, `vadd_apply`, `vadd_comp`, `zero_apply`, `zero_comp`, `zpow_apply`, `zpow_comp`, `zsmul_apply`, `zsmul_comp`, `compLeftContinuous_apply`, `compLeftContinuous_apply_apply`, `strongly`, `separatesPoints_monotone`, `algebraMap_apply`	101
Total	181

AddMonoidHom

Definitions

Name	Category	Theorems
`compLeftContinuous` 📖	CompOp	2 math math: `ContinuousLinearMap.compLeftContinuous_apply`, `compLeftContinuous_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuous_apply` 📖	mathematical	`Continuous` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `instFunLike`	`ContinuousMap` `ContinuousMap.instAddZeroClassOfContinuousAdd` `compLeftContinuous` `ContinuousMap.comp`	—	—

AlgHom

Definitions

Name	Category	Theorems
`compLeftContinuous` 📖	CompOp	3 math math: `compLeftContinuous_apply_apply`, `Subalgebra.SeparatesPoints.rclike_to_real`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuous_apply_apply` 📖	mathematical	`Continuous` `DFunLike.coe` `AlgHom` `funLike`	`ContinuousMap` `ContinuousMap.instFunLike` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `compLeftContinuous`	—	—

ContinuousFunctions

Definitions

Name	Category	Theorems
`instCoeFunElemForallSetOfContinuous` 📖	CompOp	—

ContinuousLinearMap

Definitions

Name	Category	Theorems
`compLeftContinuous` 📖	CompOp	2 math math: `compLeftContinuous_apply`, `ContinuousCohomology.I_map_hom`
`const` 📖	CompOp	2 math math: `const_apply_apply`, `ContinuousCohomology.const_app_hom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuous_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `ContinuousMap.compactOpen` `ContinuousMap.instAddCommMonoidOfContinuousAdd` `ContinuousMap.module` `funLike` `compLeftContinuous` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `ContinuousMap.instAddZeroClassOfContinuousAdd` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `AddMonoidHom.toZeroHom` `AddMonoidHom.compLeftContinuous` `LinearMap.toAddMonoidHom` `toLinearMap`	—	—
`const_apply_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap.compactOpen` `ContinuousMap.instAddCommMonoidOfContinuousAdd` `ContinuousMap.module` `funLike` `const`	—	—

ContinuousMap

Definitions

Name	Category	Theorems
`C` 📖	CompOp	1 math math: `C_apply`
`algebra` 📖	CompOp	119 math math: `polynomialFunctions.eq_adjoin_X`, `Matrix.IsHermitian.isClosedEmbedding_cfcAux`, `IsSelfAdjoint.commute_cfcHom`, `abs_mem_subalgebra_closure`, `continuousMap_mem_subalgebra_closure_of_separatesPoints`, `UnitAddTorus.mFourierSubalgebra_coe`, `toNNReal_neg_algebraMap`, `Subalgebra.SeparatesPoints.strongly`, `UnitAddTorus.mFourierSubalgebra_closure_eq_top`, `cfcHom_continuous`, `polynomialFunctions.starClosure_topologicalClosure`, `cfcL_apply`, `cfcHom_nonneg_iff`, `gelfandStarTransform_naturality`, `cfc_apply_mkD`, `Polynomial.toAddCircle_X_pow_eq_fourier`, `gelfandTransform_bijective`, `cfcHom_isClosedEmbedding`, `BoundedContinuousFunction.coe_toContinuousMapStarₐ`, `algebraMap_apply`, `cfcHom_le_iff`, `cfcHom_id`, `toNNReal_algebraMap`, `spectrum.gelfandTransform_eq`, `spectrum_eq_preimage_range`, `coeFnAlgHom_apply`, `continuousMap_mem_polynomialFunctions_closure`, `StarAlgHom.realContinuousMapOfNNReal_apply`, `gelfandStarTransform_symm_apply`, `Polynomial.toAddCircle.integrable`, `Subalgebra.separatesPoints_monotone`, `gelfandTransform_map_star`, `polynomialFunctions.starClosure_eq_adjoin_X`, `cfcHom_integral`, `compStarAlgHom_comp`, `compStarAlgHom'_comp`, `sup_mem_closed_subalgebra`, `ContinuousFunctionalCalculus.exists_cfc_of_predicate`, `cfc_def`, `fourierSubalgebra_separatesPoints`, `StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal`, `exists_mem_subalgebra_near_continuousMap_of_separatesPoints`, `adjoin_id_eq_span_one_union`, `Matrix.IsHermitian.cfcAux_apply`, `sup_mem_subalgebra_closure`, `inf_mem_subalgebra_closure`, `inf_mem_closed_subalgebra`, `exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints`, `continuous_cfcHomSuperset_left`, `cfcHomSuperset_apply`, `range_cfc_eq_range_cfcHom`, `fourierSubalgebra_coe`, `Polynomial.toAddCircle_monomial_eq_smul_fourier`, `subalgebra_topologicalClosure_eq_top_of_separatesPoints`, `cfcHom_eq_cfc_extend`, `SpectrumRestricts.starAlgHom_apply`, `UnitAddTorus.mFourierSubalgebra_separatesPoints`, `Commute.cfcHom`, `evalStarAlgHom_apply`, `Polynomial.aeval_continuousMap_apply`, `subsingleton_subalgebra`, `nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `cfc_apply`, `polynomialFunctions_coe`, `Polynomial.fourierCoeff_toAddCircle_natCast`, `spectrum_eq_range`, `Polynomial.toContinuousMapAlgHom_apply`, `StarAlgHom.realContinuousMapOfNNReal_injective`, `cfcHom_isStrictlyPositive_iff`, `BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `cfc_apply_pi`, `comp_attachBound_mem_closure`, `Matrix.IsHermitian.cfcAux_id`, `adjoin_id_eq_span_one_add`, `cfcHomSuperset_id`, `BoundedContinuousFunction.coe_toContinuousMapₐ`, `AlgHom.compLeftContinuous_apply_apply`, `WeakDual.gelfandTransform_apply_apply`, `compStarAlgHom_id`, `fourierSubalgebra_closure_eq_top`, `BoundedContinuousFunction.toContinuousMapₐ_apply`, `polynomialFunctions.topologicalClosure`, `cfcHom_predicate`, `polynomial_comp_attachBound`, `norm_cfcHom`, `evalAlgHom_apply`, `ker_evalStarAlgHom_inter_adjoin_id`, `cfcHomSuperset_continuous`, `compRightAlgHom_continuous`, `elemental_id_eq_top`, `gelfandTransform_isometry`, `polynomialFunctions_closure_eq_top'`, `compStarAlgHom'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `polynomial_comp_attachBound_mem`, `range_cfcHom`, `nnnorm_cfcHom`, `Polynomial.toAddCircle_X_eq_fourier_one`, `ker_evalStarAlgHom_eq_closure_adjoin_id`, `exists_mem_subalgebra_near_continuous_of_separatesPoints`, `compStarAlgHom_apply`, `cfcHom_mono`, `IsometricContinuousFunctionalCalculus.isometric`, `compStarAlgHom'_id`, `Polynomial.toAddCircle_C_eq_smul_fourier_zero`, `polynomialFunctions_closure_eq_top`, `BoundedContinuousFunction.separatesPoints_charPoly`, `cfcHom_eq_of_isStarNormal`, `Polynomial.fourierCoeff_toAddCircle`, `cfcHom_map_spectrum`, `compRightAlgHom_apply`, `Polynomial.toContinuousMapOnAlgHom_apply`, `cfcHom_apply_mem_elemental`, `LocallyConstant.toContinuousMapAlgHom_apply`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`, `isometry_cfcHom`, `polynomialFunctions.comap_compRightAlgHom_iccHomeoI`, `Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero`
`coeFnAddMonoidHom` 📖	CompOp	2 math math: `coeFnAddMonoidHom_apply`, `coeFnLinearMap_apply`
`coeFnAlgHom` 📖	CompOp	1 math math: `coeFnAlgHom_apply`
`coeFnLinearMap` 📖	CompOp	1 math math: `coeFnLinearMap_apply`
`coeFnMonoidHom` 📖	CompOp	1 math math: `coeFnMonoidHom_apply`
`coeFnRingHom` 📖	CompOp	1 math math: `coeFnRingHom_apply`
`compAddMonoidHom'` 📖	CompOp	1 math math: `compAddMonoidHom'_apply`
`compMonoidHom'` 📖	CompOp	1 math math: `compMonoidHom'_apply`
`compRightAlgHom` 📖	CompOp	3 math math: `compRightAlgHom_continuous`, `compRightAlgHom_apply`, `polynomialFunctions.comap_compRightAlgHom_iccHomeoI`
`evalAlgHom` 📖	CompOp	1 math math: `evalAlgHom_apply`
`evalCLM` 📖	CompOp	1 math math: `evalCLM_apply`
`instAdd` 📖	CompOp	18 math math: `addEquivBoundedOfCompact_apply`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `BoundedContinuousFunction.mkOfCompact_add`, `gelfandStarTransform_symm_apply`, `toNNReal_mul_add_neg_mul_add_mul_neg_eq`, `coe_add`, `linearIsometryBoundedOfCompact_toAddEquiv`, `Homeomorph.compStarAlgEquiv'_apply`, `add_apply`, `adjoin_id_eq_span_one_add`, `addEquivBoundedOfCompact_symm_apply`, `instContinuousAddOfLocallyCompactSpace`, `add_comp`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `toNNReal_add_add_neg_add_neg_eq`, `cfcHom_eq_of_isStarNormal`, `continuousFunctionalCalculus_map_id`
`instAddCommGroupContinuousMap` 📖	CompOp	4 math math: `ContinuousCohomology.I_obj_V_isAddCommGroup`, `ContinuousCohomology.I_obj_ρ_apply`, `ContinuousCohomology.I_map_hom`, `ContinuousCohomology.const_app_hom`
`instAddCommMonoidOfContinuousAdd` 📖	CompOp	43 math math: `toLp_inj`, `Real.fourierCoeff_tsum_comp_add`, `span_fourier_closure_eq_top`, `toLp_denseRange`, `range_toLp`, `UnitAddTorus.mFourierSubalgebra_coe`, `BoundedContinuousFunction.toContinuousMapLinearMap_apply`, `summable_of_locally_summable_norm`, `LocallyConstant.toContinuousMapLinearMap_apply`, `cfcL_apply`, `toLp_norm_le`, `cfcL_integrable`, `UnitAddTorus.mFourierCoeff_toLp`, `ContinuousLinearMap.const_apply_apply`, `periodic_tsum_comp_add_zsmul`, `evalCLM_apply`, `toLp_def`, `coeFnLinearMap_apply`, `ContinuousMapZero.toContinuousMapCLM_apply`, `instIsOrderedAddMonoid`, `adjoin_id_eq_span_one_union`, `toLp_norm_eq_toLp_norm_coe`, `fourierCoeff_toLp`, `ContinuousLinearMap.compLeftContinuous_apply`, `sum_apply`, `cfc_eq_cfcL_mkD`, `PadicInt.hasSum_mahlerSeries`, `fourierSubalgebra_coe`, `toLp_injective`, `UnitAddTorus.hasSum_mFourier_series_of_summable`, `PadicInt.hasSum_mahler`, `coe_toLp`, `cfcL_integral`, `coeFn_toLp`, `linearIsometryBoundedOfCompact_toAddEquiv`, `toLp_comp_toContinuousMap`, `adjoin_id_eq_span_one_add`, `hasSum_fourier_series_of_summable`, `instLocallyConvexSpace`, `coe_sum`, `cfc_eq_cfcL`, `UnitAddTorus.span_mFourier_closure_eq_top`, `MeasureTheory.ContinuousMap.inner_toLp`
`instAddCommSemigroupOfContinuousAdd` 📖	CompOp	—
`instAddGroupOfIsTopologicalAddGroup` 📖	CompOp	4 math math: `abs_mem_subalgebra_closure`, `instIsTopologicalAddGroup`, `abs_apply`, `coe_abs`
`instAddMonoidOfContinuousAdd` 📖	CompOp	4 math math: `addUnitsLift_apply_neg_apply`, `val_addUnitsLift_apply_apply`, `val_addUnitsLift_symm_apply_apply`, `addUnitsLift_symm_apply_apply_neg'`
`instAddMonoidWithOneOfContinuousAdd` 📖	CompOp	—
`instAddSemigroupOfContinuousAdd` 📖	CompOp	—
`instAddZeroClassOfContinuousAdd` 📖	CompOp	8 math math: `coeFnAddMonoidHom_apply`, `BoundedContinuousFunction.toContinuousMapAddMonoidHom_apply`, `coeFnLinearMap_apply`, `LocallyConstant.toContinuousMapAddMonoidHom_apply`, `ContinuousLinearMap.compLeftContinuous_apply`, `compAddMonoidHom'_apply`, `AddMonoidHom.compLeftContinuous_apply`, `addEquivBoundedOfCompact_symm_apply`
`instCommGroupContinuousMap` 📖	CompOp	—
`instCommMonoidOfContinuousMul` 📖	CompOp	5 math math: `BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq`, `prod_apply`, `instIsOrderedMonoid`, `BumpCovering.exists_finset_toPOUFun_eventuallyEq`, `coe_prod`
`instCommMonoidWithZeroOfContinuousMul` 📖	CompOp	—
`instCommRingOfIsTopologicalRing` 📖	CompOp	—
`instCommSemigroupOfContinuousMul` 📖	CompOp	—
`instCommSemiringOfIsTopologicalSemiring` 📖	CompOp	—
`instDistribMulActionOfContinuousConstSMul` 📖	CompOp	4 math math: `gelfandStarTransform_symm_apply`, `ContinuousMapZero.toContinuousMapHom_toNNReal`, `ContinuousMapZero.toContinuousMapHom_apply`, `ContinuousMapZero.coe_toContinuousMapHom`
`instDivOfContinuousDiv` 📖	CompOp	3 math math: `div_comp`, `div_apply`, `coe_div`
`instGroupOfIsTopologicalGroup` 📖	CompOp	3 math math: `instIsTopologicalGroup`, `coe_mabs`, `mabs_apply`
`instIntCast` 📖	CompOp	2 math math: `coe_intCast`, `intCast_apply`
`instInvOfContinuousInv` 📖	CompOp	3 math math: `inv_comp`, `inv_apply`, `coe_inv`
`instMonoidOfContinuousMul` 📖	CompOp	6 math math: `val_unitsLift_apply_apply`, `isUnit_iff_forall_isUnit`, `val_unitsLift_symm_apply_apply`, `unitsLift_apply_inv_apply`, `unitsLift_symm_apply_apply_inv'`, `isUnit_iff_forall_ne_zero`
`instMonoidWithZeroOfContinuousMul` 📖	CompOp	—
`instMul` 📖	CompOp	16 math math: `instContinuousMulOfLocallyCompactSpace`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `gelfandStarTransform_symm_apply`, `instSMulCommClass_2`, `toNNReal_mul_add_neg_mul_add_mul_neg_eq`, `instSMulCommClass_1`, `Homeomorph.compStarAlgEquiv'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `mul_comp`, `coe_mul`, `cfcHom_eq_of_isStarNormal`, `mul_apply`, `continuousFunctionalCalculus_map_id`, `instIsScalarTower_1`, `exists_mul_le_one_eqOn_ge`
`instMulActionOfContinuousConstSMul` 📖	CompOp	—
`instMulOneClassOfContinuousMul` 📖	CompOp	5 math math: `compMonoidHom'_apply`, `BoundedContinuousFunction.toContinuousMapMonoidHom_apply`, `LocallyConstant.toContinuousMapMonoidHom_apply`, `MonoidHom.compLeftContinuous_apply`, `coeFnMonoidHom_apply`
`instMulZeroClassOfContinuousMul` 📖	CompOp	—
`instNSMul` 📖	CompOp	3 math math: `nsmul_comp`, `coe_nsmul`, `nsmul_apply`
`instNatCast` 📖	CompOp	2 math math: `coe_natCast`, `natCast_apply`
`instNegOfContinuousNeg` 📖	CompOp	9 math math: `toNNReal_neg_algebraMap`, `StarAlgHom.realContinuousMapOfNNReal_apply`, `neg_comp`, `coe_neg`, `BoundedContinuousFunction.mkOfCompact_neg`, `toNNReal_mul_add_neg_mul_add_mul_neg_eq`, `toNNReal_neg_one`, `toNNReal_add_add_neg_add_neg_eq`, `neg_apply`
`instNonAssocRingOfIsTopologicalRing` 📖	CompOp	—
`instNonAssocSemiringOfIsTopologicalSemiring` 📖	CompOp	3 math math: `coeFnRingHom_apply`, `RingHom.compLeftContinuous_apply_apply`, `C_apply`
`instNonUnitalCommRingOfIsTopologicalRing` 📖	CompOp	—
`instNonUnitalCommSemiringOfIsTopologicalSemiring` 📖	CompOp	—
`instNonUnitalNonAssocRingOfIsTopologicalRing` 📖	CompOp	8 math math: `abs_mem_subalgebra_closure`, `continuousMap_mem_subalgebra_closure_of_separatesPoints`, `sup_mem_subalgebra_closure`, `inf_mem_subalgebra_closure`, `subalgebra_topologicalClosure_eq_top_of_separatesPoints`, `instIsTopologicalRingOfLocallyCompactSpace`, `comp_attachBound_mem_closure`, `starSubalgebra_topologicalClosure_eq_top_of_separatesPoints`
`instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` 📖	CompOp	10 math math: `gelfandStarTransform_naturality`, `WeakDual.CharacterSpace.continuousMapEval_bijective`, `gelfandStarTransform_symm_apply`, `WeakDual.CharacterSpace.homeoEval_naturality`, `instIsTopologicalSemiringOfLocallyCompactSpace`, `ContinuousMapZero.toContinuousMapHom_toNNReal`, `ContinuousMapZero.toContinuousMapHom_apply`, `WeakDual.CharacterSpace.continuousMapEval_apply_apply`, `cfcHom_eq_of_isStarNormal`, `ContinuousMapZero.coe_toContinuousMapHom`
`instNonUnitalRingOfIsTopologicalRing` 📖	CompOp	—
`instNonUnitalSemiringOfIsTopologicalSemiring` 📖	CompOp	6 math math: `instStarOrderedRingOfContinuousSqrt`, `adjoin_id_eq_span_one_union`, `nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `adjoin_id_eq_span_one_add`, `ker_evalStarAlgHom_inter_adjoin_id`, `ker_evalStarAlgHom_eq_closure_adjoin_id`
`instOne` 📖	CompOp	16 math math: `one_apply`, `UnitAddTorus.mFourier_zero`, `adjoin_id_eq_span_one_union`, `toNNReal_one`, `BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq`, `comp_one`, `one_comp`, `adjoin_id_eq_span_one_add`, `BoundedContinuousFunction.mkOfCompact_one`, `BumpCovering.exists_finset_toPOUFun_eventuallyEq`, `toNNReal_neg_one`, `coe_one`, `BumpCovering.le_one'`, `instNormOneClassOfNonempty`, `BumpCovering.coe_single`, `const_one`
`instPow` 📖	CompOp	3 math math: `pow_apply`, `pow_comp`, `coe_pow`
`instRing` 📖	CompOp	6 math math: `spectrum.gelfandTransform_eq`, `spectrum_eq_preimage_range`, `NormedSpace.exp_continuousMap_eq`, `spectrum_eq_range`, `idealOfSet_ofIdeal_eq_closure`, `idealOpensGI_choice`
`instSMul` 📖	CompOp	24 math math: `instIsScalarTower`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `instStarModule`, `gelfandStarTransform_symm_apply`, `smul_apply`, `smul_comp`, `instSMulCommClass_2`, `instContinuousSMul`, `Polynomial.toAddCircle_monomial_eq_smul_fourier`, `instIsBoundedSMul`, `UnitAddTorus.hasSum_mFourier_series_of_summable`, `instSMulCommClass_1`, `Homeomorph.compStarAlgEquiv'_apply`, `hasSum_fourier_series_of_summable`, `instIsCentralScalar`, `instContinuousConstSMul`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `coe_smul`, `Polynomial.toAddCircle_C_eq_smul_fourier_zero`, `cfcHom_eq_of_isStarNormal`, `continuousFunctionalCalculus_map_id`, `instSMulCommClass`, `instIsScalarTower_1`
`instSMul'` 📖	CompOp	4 math math: `coe_smul'`, `nnnorm_smul_const`, `smul_apply'`, `norm_smul_const`
`instSemigroupOfContinuousMul` 📖	CompOp	—
`instSemigroupWithZeroOfContinuousMul` 📖	CompOp	—
`instSemiringOfIsTopologicalSemiring` 📖	CompOp	128 math math: `polynomialFunctions.eq_adjoin_X`, `Matrix.IsHermitian.isClosedEmbedding_cfcAux`, `IsSelfAdjoint.commute_cfcHom`, `abs_mem_subalgebra_closure`, `notMem_idealOfSet`, `continuousMap_mem_subalgebra_closure_of_separatesPoints`, `UnitAddTorus.mFourierSubalgebra_coe`, `toNNReal_neg_algebraMap`, `Subalgebra.SeparatesPoints.strongly`, `UnitAddTorus.mFourierSubalgebra_closure_eq_top`, `cfcHom_continuous`, `polynomialFunctions.starClosure_topologicalClosure`, `cfcL_apply`, `cfcHom_nonneg_iff`, `gelfandStarTransform_naturality`, `cfc_apply_mkD`, `mem_idealOfSet`, `Polynomial.toAddCircle_X_pow_eq_fourier`, `gelfandTransform_bijective`, `cfcHom_isClosedEmbedding`, `BoundedContinuousFunction.coe_toContinuousMapStarₐ`, `algebraMap_apply`, `cfcHom_le_iff`, `cfcHom_id`, `toNNReal_algebraMap`, `spectrum.gelfandTransform_eq`, `coeFnAlgHom_apply`, `continuousMap_mem_polynomialFunctions_closure`, `StarAlgHom.realContinuousMapOfNNReal_apply`, `idealOfSet_closed`, `gelfandStarTransform_symm_apply`, `Polynomial.toAddCircle.integrable`, `Subalgebra.separatesPoints_monotone`, `gelfandTransform_map_star`, `polynomialFunctions.starClosure_eq_adjoin_X`, `cfcHom_integral`, `compStarAlgHom_comp`, `compStarAlgHom'_comp`, `ideal_isMaximal_iff`, `sup_mem_closed_subalgebra`, `ContinuousFunctionalCalculus.exists_cfc_of_predicate`, `cfc_def`, `fourierSubalgebra_separatesPoints`, `StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal`, `exists_mem_subalgebra_near_continuousMap_of_separatesPoints`, `adjoin_id_eq_span_one_union`, `Matrix.IsHermitian.cfcAux_apply`, `sup_mem_subalgebra_closure`, `inf_mem_subalgebra_closure`, `inf_mem_closed_subalgebra`, `exists_mem_subalgebra_near_continuous_of_isCompact_of_separatesPoints`, `continuous_cfcHomSuperset_left`, `cfcHomSuperset_apply`, `range_cfc_eq_range_cfcHom`, `fourierSubalgebra_coe`, `Polynomial.toAddCircle_monomial_eq_smul_fourier`, `subalgebra_topologicalClosure_eq_top_of_separatesPoints`, `cfcHom_eq_cfc_extend`, `SpectrumRestricts.starAlgHom_apply`, `UnitAddTorus.mFourierSubalgebra_separatesPoints`, `Commute.cfcHom`, `evalStarAlgHom_apply`, `ideal_gc`, `Polynomial.aeval_continuousMap_apply`, `subsingleton_subalgebra`, `nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `cfc_apply`, `setOfTop_eq_univ`, `polynomialFunctions_coe`, `Polynomial.fourierCoeff_toAddCircle_natCast`, `Polynomial.toContinuousMapAlgHom_apply`, `StarAlgHom.realContinuousMapOfNNReal_injective`, `cfcHom_isStrictlyPositive_iff`, `BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `cfc_apply_pi`, `comp_attachBound_mem_closure`, `Matrix.IsHermitian.cfcAux_id`, `adjoin_id_eq_span_one_add`, `cfcHomSuperset_id`, `BoundedContinuousFunction.coe_toContinuousMapₐ`, `AlgHom.compLeftContinuous_apply_apply`, `WeakDual.gelfandTransform_apply_apply`, `compStarAlgHom_id`, `fourierSubalgebra_closure_eq_top`, `BoundedContinuousFunction.toContinuousMapₐ_apply`, `mem_setOfIdeal`, `polynomialFunctions.topologicalClosure`, `cfcHom_predicate`, `idealOfEmpty_eq_bot`, `polynomial_comp_attachBound`, `norm_cfcHom`, `evalAlgHom_apply`, `ker_evalStarAlgHom_inter_adjoin_id`, `cfcHomSuperset_continuous`, `compRightAlgHom_continuous`, `elemental_id_eq_top`, `gelfandTransform_isometry`, `polynomialFunctions_closure_eq_top'`, `mem_idealOfSet_compl_singleton`, `compStarAlgHom'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `polynomial_comp_attachBound_mem`, `range_cfcHom`, `nnnorm_cfcHom`, `Polynomial.toAddCircle_X_eq_fourier_one`, `ker_evalStarAlgHom_eq_closure_adjoin_id`, `idealOf_compl_singleton_isMaximal`, `exists_mem_subalgebra_near_continuous_of_separatesPoints`, `compStarAlgHom_apply`, `cfcHom_mono`, `IsometricContinuousFunctionalCalculus.isometric`, `compStarAlgHom'_id`, `Polynomial.toAddCircle_C_eq_smul_fourier_zero`, `polynomialFunctions_closure_eq_top`, `BoundedContinuousFunction.separatesPoints_charPoly`, `cfcHom_eq_of_isStarNormal`, `Polynomial.fourierCoeff_toAddCircle`, `cfcHom_map_spectrum`, `compRightAlgHom_apply`, `idealOfSet_isMaximal_iff`, `Polynomial.toContinuousMapOnAlgHom_apply`, `cfcHom_apply_mem_elemental`, `LocallyConstant.toContinuousMapAlgHom_apply`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`, `isometry_cfcHom`, `polynomialFunctions.comap_compRightAlgHom_iccHomeoI`, `Polynomial.fourierCoeff_toAddCircle_eq_zero_of_lt_zero`
`instSubOfContinuousSub` 📖	CompOp	8 math math: `coe_sub`, `exists_mem_subalgebra_near_continuousMap_of_separatesPoints`, `exists_polynomial_near_continuousMap`, `BumpCovering.exists_finset_toPartitionOfUnity_eventuallyEq`, `sub_comp`, `BumpCovering.exists_finset_toPOUFun_eventuallyEq`, `BoundedContinuousFunction.mkOfCompact_sub`, `sub_apply`
`instVAdd` 📖	CompOp	6 math math: `instContinuousVAdd`, `vadd_comp`, `coe_vadd`, `instVAddCommClass`, `vadd_apply`, `instContinuousConstVAdd`
`instZPow` 📖	CompOp	3 math math: `zpow_apply`, `zpow_comp`, `coe_zpow`
`instZSMul` 📖	CompOp	3 math math: `coe_zsmul`, `zsmul_comp`, `zsmul_apply`
`instZero` 📖	CompOp	15 math math: `toNNReal_neg_algebraMap`, `cfcHom_nonneg_iff`, `PartitionOfUnity.nonneg'`, `cfc_apply_mkD`, `BoundedContinuousFunction.mkOfCompact_zero`, `coe_zero`, `BumpCovering.nonneg'`, `cfc_eq_cfcL_mkD`, `comp_zero`, `zero_apply`, `instIsBoundedSMul`, `toNNReal_neg_one`, `zero_comp`, `const_zero`, `BumpCovering.coe_single`
`module'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`C_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `instNonAssocSemiringOfIsTopologicalSemiring` `RingHom.instFunLike` `C` `algebraMap`	—	—
`add_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instAdd`	—	—
`add_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instAdd`	—	—
`coeFnAddMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ContinuousMap` `AddZeroClass.toAddZero` `instAddZeroClassOfContinuousAdd` `AddMonoid.toAddZeroClass` `Pi.addZeroClass` `AddMonoidHom.instFunLike` `coeFnAddMonoidHom` `instFunLike`	—	—
`coeFnAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `Pi.semiring` `algebra` `Function.algebra` `AlgHom.funLike` `coeFnAlgHom` `instFunLike`	—	—
`coeFnLinearMap_apply` 📖	mathematical	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `instAddCommMonoidOfContinuousAdd` `Pi.addCommMonoid` `module` `Pi.Function.module` `LinearMap.instFunLike` `coeFnLinearMap` `ZeroHom.toFun` `AddZero.toZero` `AddZeroClass.toAddZero` `instAddZeroClassOfContinuousAdd` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Pi.addZeroClass` `AddMonoidHom.toZeroHom` `coeFnAddMonoidHom`	—	—
`coeFnMonoidHom_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `ContinuousMap` `MulOneClass.toMulOne` `instMulOneClassOfContinuousMul` `Monoid.toMulOneClass` `Pi.mulOneClass` `MonoidHom.instFunLike` `coeFnMonoidHom` `instFunLike`	—	—
`coeFnRingHom_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `ContinuousMap` `instNonAssocSemiringOfIsTopologicalSemiring` `Semiring.toNonAssocSemiring` `Pi.nonAssocSemiring` `RingHom.instFunLike` `coeFnRingHom` `instFunLike`	—	—
`coe_add` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instAdd` `Pi.instAdd`	—	—
`coe_div` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instDivOfContinuousDiv` `Pi.instDiv`	—	—
`coe_intCast` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instIntCast` `Pi.instIntCast`	—	—
`coe_inv` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instInvOfContinuousInv` `Pi.instInv`	—	—
`coe_mul` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instMul` `Pi.instMul`	—	—
`coe_natCast` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instNatCast` `Pi.instNatCast`	—	—
`coe_neg` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instNegOfContinuousNeg` `Pi.instNeg`	—	—
`coe_nsmul` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instNSMul` `Pi.instSMul` `AddMonoid.toNatSMul`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instOne` `Pi.instOne`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instPow` `Pi.instPow` `Monoid.toNatPow`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.prod` `instCommMonoidOfContinuousMul` `Pi.commMonoid`	—	`map_prod` `MonoidHom.instMonoidHomClass`
`coe_smul` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instSMul` `Function.hasSMul`	—	—
`coe_smul'` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instSMul'` `Pi.smul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`coe_sub` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instSubOfContinuousSub` `Pi.instSub`	—	—
`coe_sum` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.sum` `instAddCommMonoidOfContinuousAdd` `Pi.addCommMonoid`	—	`map_sum` `AddMonoidHom.instAddMonoidHomClass`
`coe_vadd` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `instVAdd` `Function.hasVAdd`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instZero` `Pi.instZero`	—	—
`coe_zpow` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instZPow` `Pi.instPow` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	—
`coe_zsmul` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instZSMul` `Pi.instSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	—
`compAddMonoidHom'_apply` 📖	mathematical	—	`DFunLike.coe` `AddMonoidHom` `ContinuousMap` `AddZeroClass.toAddZero` `instAddZeroClassOfContinuousAdd` `AddMonoidHom.instFunLike` `compAddMonoidHom'` `comp`	—	—
`compMonoidHom'_apply` 📖	mathematical	—	`DFunLike.coe` `MonoidHom` `ContinuousMap` `MulOneClass.toMulOne` `instMulOneClassOfContinuousMul` `MonoidHom.instFunLike` `compMonoidHom'` `comp`	—	—
`compRightAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `AlgHom.funLike` `compRightAlgHom` `comp`	—	—
`compRightAlgHom_continuous` 📖	mathematical	—	`Continuous` `ContinuousMap` `compactOpen` `DFunLike.coe` `AlgHom` `instSemiringOfIsTopologicalSemiring` `algebra` `AlgHom.funLike` `compRightAlgHom`	—	`continuous_precomp`
`comp_one` 📖	mathematical	—	`comp` `ContinuousMap` `instOne` `const` `DFunLike.coe` `instFunLike`	—	—
`comp_zero` 📖	mathematical	—	`comp` `ContinuousMap` `instZero` `const` `DFunLike.coe` `instFunLike`	—	—
`const_one` 📖	mathematical	—	`const` `ContinuousMap` `instOne`	—	—
`const_zero` 📖	mathematical	—	`const` `ContinuousMap` `instZero`	—	—
`div_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instDivOfContinuousDiv`	—	—
`div_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instDivOfContinuousDiv`	—	—
`evalAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `algebra` `AlgHom.funLike` `evalAlgHom` `instFunLike`	—	—
`evalCLM_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousLinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `ContinuousMap` `compactOpen` `instAddCommMonoidOfContinuousAdd` `module` `ContinuousLinearMap.funLike` `evalCLM` `instFunLike`	—	—
`hasProd_apply` 📖	mathematical	`HasProd` `ContinuousMap` `instCommMonoidOfContinuousMul` `compactOpen`	`DFunLike.coe` `instFunLike`	—	`HasProd.map` `MonoidHom.instMonoidHomClass` `ContinuousEvalConst.continuous_eval_const` `instContinuousEvalConst`
`hasSum_apply` 📖	mathematical	`HasSum` `ContinuousMap` `instAddCommMonoidOfContinuousAdd` `compactOpen`	`DFunLike.coe` `instFunLike`	—	`HasSum.map` `AddMonoidHom.instAddMonoidHomClass` `ContinuousEvalConst.continuous_eval_const` `instContinuousEvalConst`
`instContinuousAddOfLocallyCompactSpace` 📖	mathematical	—	`ContinuousAdd` `ContinuousMap` `compactOpen` `instAdd`	—	`continuous_of_continuous_uncurry` `Continuous.comp` `ContinuousEval.continuous_eval` `instContinuousEvalOfLocallyCompactPair` `instLocallyCompactPairOfLocallyCompactSpace` `Continuous.prodMap` `continuous_fst` `continuous_id` `continuous_snd` `Continuous.add`
`instContinuousConstSMul` 📖	mathematical	—	`ContinuousConstSMul` `ContinuousMap` `compactOpen` `instSMul`	—	`continuous_postcomp` `ContinuousConstSMul.continuous_const_smul`
`instContinuousConstVAdd` 📖	mathematical	—	`ContinuousConstVAdd` `ContinuousMap` `compactOpen` `instVAdd`	—	`continuous_postcomp` `ContinuousConstVAdd.continuous_const_vadd`
`instContinuousMulOfLocallyCompactSpace` 📖	mathematical	—	`ContinuousMul` `ContinuousMap` `compactOpen` `instMul`	—	`continuous_of_continuous_uncurry` `Continuous.comp` `ContinuousEval.continuous_eval` `instContinuousEvalOfLocallyCompactPair` `instLocallyCompactPairOfLocallyCompactSpace` `Continuous.prodMap` `continuous_fst` `continuous_id` `continuous_snd` `Continuous.mul`
`instContinuousSMul` 📖	mathematical	—	`ContinuousSMul` `ContinuousMap` `instSMul` `ContinuousSMul.continuousConstSMul` `compactOpen`	—	`ContinuousSMul.continuousConstSMul` `Continuous.comp` `ContinuousSMul.continuous_smul` `continuous_postcomp` `continuous_prodMk_const`
`instContinuousVAdd` 📖	mathematical	—	`ContinuousVAdd` `ContinuousMap` `instVAdd` `ContinuousVAdd.continuousConstVAdd` `compactOpen`	—	`ContinuousVAdd.continuousConstVAdd` `Continuous.comp` `ContinuousVAdd.continuous_vadd` `continuous_postcomp` `continuous_prodMk_const`
`instIsCentralScalar` 📖	mathematical	—	`IsCentralScalar` `ContinuousMap` `instSMul` `MulOpposite` `ContinuousConstSMul.op`	—	`ContinuousConstSMul.op` `ext` `IsCentralScalar.op_smul_eq_smul`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `ContinuousMap` `instSMul`	—	`ext` `smul_assoc`
`instIsScalarTower_1` 📖	mathematical	—	`IsScalarTower` `ContinuousMap` `instSMul` `instMul`	—	`ext` `smul_mul_assoc`
`instIsTopologicalAddGroup` 📖	mathematical	—	`IsTopologicalAddGroup` `ContinuousMap` `compactOpen` `instAddGroupOfIsTopologicalAddGroup` `AddCommGroup.toAddGroup`	—	`isUniformAddGroup_of_addCommGroup` `continuous_iff_continuousAt` `ContinuousAt.eq_1` `tendsto_iff_forall_isCompact_tendstoUniformlyOn` `nhds_prod_eq` `UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_add` `TendstoUniformlyOn.prodMk` `Filter.tendsto_id` `uniformContinuous_neg`
`instIsTopologicalGroup` 📖	mathematical	—	`IsTopologicalGroup` `ContinuousMap` `compactOpen` `instGroupOfIsTopologicalGroup` `CommGroup.toGroup`	—	`isUniformGroup_of_commGroup` `continuous_iff_continuousAt` `ContinuousAt.eq_1` `tendsto_iff_forall_isCompact_tendstoUniformlyOn` `nhds_prod_eq` `UniformContinuous.comp_tendstoUniformlyOn` `uniformContinuous_mul` `TendstoUniformlyOn.prodMk` `Filter.tendsto_id` `uniformContinuous_inv`
`instIsTopologicalRingOfLocallyCompactSpace` 📖	mathematical	—	`IsTopologicalRing` `ContinuousMap` `compactOpen` `instNonUnitalNonAssocRingOfIsTopologicalRing` `NonUnitalRing.toNonUnitalNonAssocRing`	—	`instIsTopologicalSemiringOfLocallyCompactSpace` `IsTopologicalRing.toIsTopologicalSemiring` `IsTopologicalAddGroup.toContinuousNeg` `IsTopologicalRing.to_topologicalAddGroup` `instIsTopologicalAddGroup`
`instIsTopologicalSemiringOfLocallyCompactSpace` 📖	mathematical	—	`IsTopologicalSemiring` `ContinuousMap` `compactOpen` `instNonUnitalNonAssocSemiringOfIsTopologicalSemiring` `NonUnitalSemiring.toNonUnitalNonAssocSemiring`	—	`instContinuousAddOfLocallyCompactSpace` `IsTopologicalSemiring.toContinuousAdd` `instContinuousMulOfLocallyCompactSpace` `IsTopologicalSemiring.toContinuousMul`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `ContinuousMap` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`instSMulCommClass_1` 📖	mathematical	—	`SMulCommClass` `ContinuousMap` `instSMul` `instMul`	—	`ext` `mul_smul_comm`
`instSMulCommClass_2` 📖	mathematical	—	`SMulCommClass` `ContinuousMap` `instMul` `instSMul`	—	`ext` `SMulCommClass.smul_comm`
`instVAddCommClass` 📖	mathematical	—	`VAddCommClass` `ContinuousMap` `instVAdd`	—	`ext` `VAddCommClass.vadd_comm`
`intCast_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instIntCast`	—	—
`inv_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instInvOfContinuousInv`	—	—
`inv_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instInvOfContinuousInv`	—	—
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instMul`	—	—
`mul_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instMul`	—	—
`multipliable_apply` 📖	mathematical	`Multipliable` `ContinuousMap` `instCommMonoidOfContinuousMul` `compactOpen`	`DFunLike.coe` `instFunLike`	—	`HasProd.multipliable` `hasProd_apply` `Multipliable.hasProd`
`natCast_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instNatCast`	—	—
`neg_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instNegOfContinuousNeg`	—	—
`neg_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instNegOfContinuousNeg`	—	—
`nsmul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instNSMul` `AddMonoid.toNatSMul`	—	—
`nsmul_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instNSMul`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instOne`	—	—
`one_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instOne`	—	—
`pow_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instPow` `Monoid.toNatPow`	—	—
`pow_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instPow`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.prod` `instCommMonoidOfContinuousMul`	—	`coe_prod` `Finset.prod_apply`
`smul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instSMul`	—	—
`smul_apply'` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instSMul'` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	—
`smul_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instSMul`	—	—
`sub_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instSubOfContinuousSub`	—	—
`sub_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instSubOfContinuousSub`	—	—
`subsingleton_subalgebra` 📖	mathematical	—	`Subalgebra` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `algebra` `Algebra.id`	—	`isEmpty_or_nonempty` `Function.Injective.subsingleton` `DFunLike.coe_injective` `Unique.instSubsingleton` `Subalgebra.subsingleton_of_subsingleton` `Subalgebra.ext` `ext` `algebraMap_apply` `mul_one`
`sum_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `Finset.sum` `instAddCommMonoidOfContinuousAdd`	—	`coe_sum` `Finset.sum_apply`
`summable_apply` 📖	mathematical	`Summable` `ContinuousMap` `instAddCommMonoidOfContinuousAdd` `compactOpen`	`DFunLike.coe` `instFunLike`	—	`HasSum.summable` `hasSum_apply` `Summable.hasSum`
`tprod_apply` 📖	mathematical	`Multipliable` `ContinuousMap` `instCommMonoidOfContinuousMul` `compactOpen`	`tprod` `DFunLike.coe` `instFunLike`	—	`HasProd.tprod_eq` `hasProd_apply` `Multipliable.hasProd`
`tsum_apply` 📖	mathematical	`Summable` `ContinuousMap` `instAddCommMonoidOfContinuousAdd` `compactOpen`	`tsum` `DFunLike.coe` `instFunLike`	—	`HasSum.tsum_eq` `hasSum_apply` `Summable.hasSum`
`vadd_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `HVAdd.hVAdd` `instHVAdd` `instVAdd`	—	—
`vadd_comp` 📖	mathematical	—	`comp` `HVAdd.hVAdd` `ContinuousMap` `instHVAdd` `instVAdd`	—	—
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instZero`	—	—
`zero_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instZero`	—	—
`zpow_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instZPow` `DivInvMonoid.toZPow` `Group.toDivInvMonoid`	—	—
`zpow_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instZPow`	—	—
`zsmul_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `instZSMul` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid`	—	—
`zsmul_comp` 📖	mathematical	—	`comp` `ContinuousMap` `instZSMul`	—	—

MonoidHom

Definitions

Name	Category	Theorems
`compLeftContinuous` 📖	CompOp	1 math math: `compLeftContinuous_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuous_apply` 📖	mathematical	`Continuous` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instFunLike`	`ContinuousMap` `ContinuousMap.instMulOneClassOfContinuousMul` `compLeftContinuous` `ContinuousMap.comp`	—	—

RingHom

Definitions

Name	Category	Theorems
`compLeftContinuous` 📖	CompOp	1 math math: `compLeftContinuous_apply_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compLeftContinuous_apply_apply` 📖	mathematical	`Continuous` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instFunLike`	`ContinuousMap` `ContinuousMap.instFunLike` `ContinuousMap.instNonAssocSemiringOfIsTopologicalSemiring` `compLeftContinuous`	—	—

Set

Definitions

Name	Category	Theorems
`SeparatesPointsStrongly` 📖	MathDef	1 math math: `Subalgebra.SeparatesPoints.strongly`

Subalgebra

Definitions

Name	Category	Theorems
`SeparatesPoints` 📖	MathDef	5 math math: `polynomialFunctions_separatesPoints`, `separatesPoints_monotone`, `fourierSubalgebra_separatesPoints`, `UnitAddTorus.mFourierSubalgebra_separatesPoints`, `BoundedContinuousFunction.separatesPoints_charPoly`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`separatesPoints_monotone` 📖	mathematical	—	`Monotone` `Subalgebra` `ContinuousMap` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `PartialOrder.toPreorder` `instPartialOrder` `Prop.partialOrder` `SeparatesPoints`	—	—

Subalgebra.SeparatesPoints

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`strongly` 📖	mathematical	`Subalgebra.SeparatesPoints` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.id` `IsTopologicalRing.toIsTopologicalSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Field.toCommRing`	`Set.SeparatesPointsStrongly` `SetLike.coe` `Subalgebra` `ContinuousMap` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `Subalgebra.instSetLike`	—	`IsTopologicalRing.toIsTopologicalSemiring` `AddSubmonoidWithOneClass.toOneMemClass` `IsTopologicalSemiring.toContinuousAdd` `SubsemiringClass.addSubmonoidWithOneClass` `Subalgebra.instSubsemiringClass` `Subtype.prop` `mul_one` `sub_ne_zero_of_ne` `IsTopologicalRing.to_topologicalAddGroup` `SubringClass.addSubgroupClass` `Subalgebra.instSubringClass` `algebraMap_apply` `sub_self` `MulZeroClass.mul_zero` `zero_add` `inv_mul_cancel_right₀` `sub_add_cancel`

(root)

Definitions

Name	Category	Theorems
`continuousAddSubgroup` 📖	CompOp	—
`continuousAddSubmonoid` 📖	CompOp	—
`continuousSubalgebra` 📖	CompOp	—
`continuousSubgroup` 📖	CompOp	—
`continuousSubmodule` 📖	CompOp	—
`continuousSubmonoid` 📖	CompOp	—
`continuousSubring` 📖	CompOp	—
`continuousSubsemiring` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`algebraMap_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `RingHom.instFunLike` `algebraMap` `ContinuousMap.algebra` `Algebra.toSMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`Algebra.algebraMap_eq_smul_one`

---

← Back to Index