Documentation Verification Report

Star

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

Statistics

Metric	Count
Definitions `compStarAlgHom`, `compStarAlgHom'`, `evalStarAlgHom`, `instInvolutiveStarOfContinuousStar`, `instStar`, `instStarRingOfContinuousStar`, `starAddMonoid`, `starMul`, `compStarAlgEquiv'`, `Star`, `Star`	11
Theorems `coe_star`, `compStarAlgHom'_apply`, `compStarAlgHom'_comp`, `compStarAlgHom'_id`, `compStarAlgHom_apply`, `compStarAlgHom_comp`, `compStarAlgHom_id`, `evalStarAlgHom_apply`, `instStarModule`, `instTrivialStar`, `star_apply`, `compStarAlgEquiv'_apply`, `compStarAlgEquiv'_symm_apply`	13
Total	24

ContinuousMap

Definitions

Name	Category	Theorems
`compStarAlgHom` 📖	CompOp	3 math math: `compStarAlgHom_comp`, `compStarAlgHom_id`, `compStarAlgHom_apply`
`compStarAlgHom'` 📖	CompOp	7 math math: `gelfandStarTransform_naturality`, `WeakDual.CharacterSpace.homeoEval_naturality`, `compStarAlgHom'_comp`, `Homeomorph.compStarAlgEquiv'_apply`, `compStarAlgHom'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `compStarAlgHom'_id`
`evalStarAlgHom` 📖	CompOp	4 math math: `evalStarAlgHom_apply`, `nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `ker_evalStarAlgHom_inter_adjoin_id`, `ker_evalStarAlgHom_eq_closure_adjoin_id`
`instInvolutiveStarOfContinuousStar` 📖	CompOp	—
`instStar` 📖	CompOp	63 math math: `Matrix.IsHermitian.isClosedEmbedding_cfcAux`, `IsSelfAdjoint.commute_cfcHom`, `BoundedContinuousFunction.mkOfCompact_star`, `cfcHom_continuous`, `cfcL_apply`, `cfcHom_nonneg_iff`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `cfc_apply_mkD`, `instStarModule`, `cfcHom_isClosedEmbedding`, `BoundedContinuousFunction.coe_toContinuousMapStarₐ`, `cfcHom_le_iff`, `cfcHom_id`, `StarAlgHom.realContinuousMapOfNNReal_apply`, `gelfandStarTransform_symm_apply`, `gelfandTransform_map_star`, `cfcHom_integral`, `compStarAlgHom_comp`, `compStarAlgHom'_comp`, `ContinuousFunctionalCalculus.exists_cfc_of_predicate`, `cfc_def`, `StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal`, `Matrix.IsHermitian.cfcAux_apply`, `continuous_cfcHomSuperset_left`, `cfcHomSuperset_apply`, `ContinuousMapZero.toContinuousMapHom_toNNReal`, `cfcHom_eq_cfc_extend`, `star_apply`, `SpectrumRestricts.starAlgHom_apply`, `Commute.cfcHom`, `evalStarAlgHom_apply`, `nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `cfc_apply`, `StarAlgHom.realContinuousMapOfNNReal_injective`, `cfcHom_isStrictlyPositive_iff`, `BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `cfc_apply_pi`, `ContinuousMapZero.toContinuousMapHom_apply`, `Matrix.IsHermitian.cfcAux_id`, `coe_star`, `cfcHomSuperset_id`, `compStarAlgHom_id`, `cfcHom_predicate`, `norm_cfcHom`, `ker_evalStarAlgHom_inter_adjoin_id`, `cfcHomSuperset_continuous`, `compStarAlgHom'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `nnnorm_cfcHom`, `ker_evalStarAlgHom_eq_closure_adjoin_id`, `compStarAlgHom_apply`, `cfcHom_mono`, `IsometricContinuousFunctionalCalculus.isometric`, `compStarAlgHom'_id`, `cfcHom_eq_of_isStarNormal`, `ContinuousMapZero.coe_toContinuousMapHom`, `cfcHom_map_spectrum`, `continuousFunctionalCalculus_map_id`, `cfcHom_apply_mem_elemental`, `instTrivialStar`, `isometry_cfcHom`
`instStarRingOfContinuousStar` 📖	CompOp	22 math math: `UnitAddTorus.mFourierSubalgebra_coe`, `UnitAddTorus.mFourierSubalgebra_closure_eq_top`, `polynomialFunctions.starClosure_topologicalClosure`, `polynomialFunctions.starClosure_le_equalizer`, `WeakDual.CharacterSpace.homeoEval_naturality`, `polynomialFunctions.starClosure_eq_adjoin_X`, `instStarOrderedRingOfContinuousSqrt`, `fourierSubalgebra_separatesPoints`, `adjoin_id_eq_span_one_union`, `instCStarRing`, `range_cfc_eq_range_cfcHom`, `fourierSubalgebra_coe`, `UnitAddTorus.mFourierSubalgebra_separatesPoints`, `nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `adjoin_id_eq_span_one_add`, `fourierSubalgebra_closure_eq_top`, `ker_evalStarAlgHom_inter_adjoin_id`, `elemental_id_eq_top`, `range_cfcHom`, `ker_evalStarAlgHom_eq_closure_adjoin_id`, `BoundedContinuousFunction.separatesPoints_charPoly`, `RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict`
`starAddMonoid` 📖	CompOp	6 math math: `UnitAddTorus.mFourierSubalgebra_closure_eq_top`, `polynomialFunctions.starClosure_topologicalClosure`, `instNormedStarGroup`, `fourierSubalgebra_closure_eq_top`, `elemental_id_eq_top`, `starSubalgebra_topologicalClosure_eq_top_of_separatesPoints`
`starMul` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_star` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `Star.star` `instStar` `Pi.instStarForall`	—	—
`compStarAlgHom'_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `instStar` `StarAlgHom.instFunLike` `compStarAlgHom'` `comp`	—	—
`compStarAlgHom'_comp` 📖	mathematical	—	`compStarAlgHom'` `comp` `StarAlgHom.comp` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `instStar`	—	`StarAlgHom.ext` `ext`
`compStarAlgHom'_id` 📖	mathematical	—	`compStarAlgHom'` `id` `StarAlgHom.id` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `instStar`	—	`StarAlgHom.ext` `ext`
`compStarAlgHom_apply` 📖	mathematical	`Continuous` `DFunLike.coe` `StarAlgHom` `StarAlgHom.instFunLike`	`ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `instStar` `compStarAlgHom` `comp`	—	—
`compStarAlgHom_comp` 📖	mathematical	`Continuous` `DFunLike.coe` `StarAlgHom` `StarAlgHom.instFunLike`	`compStarAlgHom` `StarAlgHom.comp` `Continuous.comp` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `StarAlgHom.toAlgHom` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `instStar`	—	`Continuous.comp`
`compStarAlgHom_id` 📖	mathematical	—	`compStarAlgHom` `StarAlgHom.id` `continuous_id` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `algebra` `instStar`	—	`continuous_id`
`evalStarAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `ContinuousMap` `instSemiringOfIsTopologicalSemiring` `CommSemiring.toSemiring` `algebra` `instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarAlgHom.instFunLike` `evalStarAlgHom` `instFunLike`	—	—
`instStarModule` 📖	mathematical	—	`StarModule` `ContinuousMap` `instStar` `instSMul`	—	`ext` `StarModule.star_smul`
`instTrivialStar` 📖	mathematical	—	`TrivialStar` `ContinuousMap` `instStar`	—	`ext` `TrivialStar.star_trivial`
`star_apply` 📖	mathematical	—	`DFunLike.coe` `ContinuousMap` `instFunLike` `Star.star` `instStar`	—	—

Homeomorph

Definitions

Name	Category	Theorems
`compStarAlgEquiv'` 📖	CompOp	2 math math: `compStarAlgEquiv'_apply`, `compStarAlgEquiv'_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`compStarAlgEquiv'_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `ContinuousMap` `ContinuousMap.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMap.instMul` `Distrib.toMul` `IsTopologicalSemiring.toContinuousMul` `ContinuousMap.instSMul` `Algebra.toSMul` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.to_smulCommClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `StarAlgEquiv.instFunLike` `compStarAlgEquiv'` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `StarAlgHom.instFunLike` `ContinuousMap.compStarAlgHom'` `toContinuousMap` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `instContinuousMapClass`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass`
`compStarAlgEquiv'_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `ContinuousMap` `ContinuousMap.instAdd` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `IsTopologicalSemiring.toContinuousAdd` `ContinuousMap.instMul` `Distrib.toMul` `IsTopologicalSemiring.toContinuousMul` `ContinuousMap.instSMul` `Algebra.toSMul` `SMulCommClass.continuousConstSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Algebra.to_smulCommClass` `NonUnitalSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonUnitalSemiring` `ContinuousMap.instStar` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `StarRing.toStarAddMonoid` `StarAlgEquiv.instFunLike` `StarAlgEquiv.symm` `compStarAlgEquiv'` `StarAlgHom` `ContinuousMap.instSemiringOfIsTopologicalSemiring` `ContinuousMap.algebra` `StarAlgHom.instFunLike` `ContinuousMap.compStarAlgHom'` `toContinuousMap` `Homeomorph` `EquivLike.toFunLike` `instEquivLike` `instContinuousMapClass` `symm`	—	`IsTopologicalSemiring.toContinuousAdd` `IsTopologicalSemiring.toContinuousMul` `SMulCommClass.continuousConstSMul` `Algebra.to_smulCommClass`

Quiver

Definitions

Name	Category	Theorems
`Star` 📖	CompOp	12 math math: `starEquivCostar_symm_apply_fst`, `starEquivCostar_apply_fst`, `Prefunctor.IsCovering.star_bijective`, `starEquivCostar_apply_snd`, `Prefunctor.costar_conj_star`, `starEquivCostar_symm_apply`, `Prefunctor.symmetrifyStar`, `starEquivCostar_apply`, `Prefunctor.symmetrifyCostar`, `starEquivCostar_symm_apply_snd`, `Prefunctor.star_comp`, `Prefunctor.bijective_costar_iff_bijective_star`

(root)

Definitions

Name	Category	Theorems
`Star` 📖	CompData	—

---

← Back to Index