| Metric | Count |
|---|
DefinitionstoStarSubalgebra, ofInjective, restrictScalars, codRestrict, equalizer, range, rangeRestrict, restrictScalars, adjoin, adjoinCommRingOfComm, adjoinCommRingOfIsStarNormal, adjoinCommSemiringOfComm, adjoinCommSemiringOfIsStarNormal, gi, algebra, centralizer, comap, completeLattice, copy, inclusion, inhabited, instPartialOrder, map, ofClass, setLike, starRing, subtype, toNonUnitalStarSubalgebra, toSubalgebra, involutiveStar, starClosure | 31 |
Theoremsadjoin_le_starAlgebra_adjoin, toStarSubalgebra_toNonUnitalStarSubalgebra, ofInjective_apply, ofInjective_symm_apply, restrictScalars_apply, restrictScalars_injective, restrictScalars_symm_apply, adjoin_le_equalizer, coe_codRestrict, ext_adjoin, ext_adjoin_singleton, ext_of_adjoin_eq_top, injective_codRestrict, map_adjoin, mem_equalizer, range_eq_map_top, restrictScalars_apply, restrictScalars_injective, subtype_comp_codRestrict, adjoin_eq, adjoin_eq_span, adjoin_eq_starClosure_adjoin, adjoin_induction, adjoin_induction_subtype, adjoin_induction₂, adjoin_le, adjoin_le_centralizer_centralizer, adjoin_le_iff, adjoin_mono, adjoin_nonUnitalStarSubalgebra, adjoin_nonUnitalStarSubalgebra_eq_span, adjoin_toSubalgebra, gc, mem_adjoin_of_mem, self_mem_adjoin_singleton, star_self_mem_adjoin_singleton, star_subset_adjoin, subset_adjoin, algebraMap_mem, bot_toSubalgebra, centralizer_le, centralizer_toSubalgebra, coe_bot, coe_centralizer, coe_centralizer_centralizer, coe_comap, coe_copy, coe_iInf, coe_inf, coe_map, coe_mk, coe_sInf, coe_subtype, coe_toSubalgebra, coe_top, comap_comap, comap_id, comap_injective, comap_mono, copy_eq, eq_top_iff, ext, ext_iff, gc_map_comap, iInf_toSubalgebra, inclusion_apply, inclusion_injective, inf_toSubalgebra, instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar, map_iInf, map_id, map_inf, map_injective, map_le_iff_le_comap, map_map, map_mono, map_sup, map_toSubalgebra, mem_bot, mem_carrier, mem_centralizer_iff, mem_comap, mem_iInf, mem_inf, mem_map, mem_sInf, mem_sup_left, mem_sup_right, mem_toSubalgebra, mem_top, mul_mem_sup, ofClass_carrier, one_mem_toNonUnitalStarSubalgebra, rangeS_le, range_le, range_subset, sInf_toSubalgebra, smulMemClass, smul_mem, starMemClass, starModule, star_mem', subringClass, subsemiringClass, subtype_apply, subtype_comp_inclusion, toNonUnitalStarSubalgebra_toStarSubalgebra, toSubalgebra_eq_top, toSubalgebra_inj, toSubalgebra_injective, toSubalgebra_le_iff, toSubalgebra_subtype, top_toSubalgebra, coe_star, coe_starClosure, mem_starClosure, mem_star_iff, starClosure_eq_adjoin, starClosure_le, starClosure_le_iff, starClosure_toSubalgebra, star_adjoin_comm, star_mem_star_iff, star_mono | 124 |
| Total | 155 |
| Name | Category | Theorems |
|---|
algebra 📖 | CompOp | 19 mathmath: StarAlgEquiv.ofInjective_symm_apply, inclusion_apply, NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe, subtype_comp_inclusion, StarAlgEquiv.ofInjective_apply, StarAlgHom.coe_codRestrict, subtype_apply, isClosedEmbedding_inclusion, spectrum_eq, coe_subtype, starModule, mem_spectrum_iff, toSubalgebra_subtype, StarAlgHom.subtype_comp_codRestrict, inclusion_injective, cfcHom_eq_of_isStarNormal, StarAlgHom.injective_codRestrict, isEmbedding_inclusion, continuousFunctionalCalculus_map_id
|
centralizer 📖 | CompOp | 8 mathmath: centralizer_toSubalgebra, StarAlgebra.elemental.le_centralizer_centralizer, StarAlgebra.adjoin_le_centralizer_centralizer, topologicalClosure_adjoin_le_centralizer_centralizer, centralizer_le, coe_centralizer_centralizer, mem_centralizer_iff, coe_centralizer
|
comap 📖 | CompOp | 8 mathmath: comap_mono, mem_comap, gc_map_comap, comap_injective, comap_id, comap_comap, coe_comap, map_le_iff_le_comap
|
completeLattice 📖 | CompOp | 29 mathmath: coe_sInf, map_inf, mem_sup_left, inf_toSubalgebra, UnitAddTorus.mFourierSubalgebra_closure_eq_top, polynomialFunctions.starClosure_topologicalClosure, bot_toSubalgebra, mem_bot, mul_mem_sup, eq_top_iff, coe_bot, mem_iInf, toSubalgebra_eq_top, mem_top, map_sup, sInf_toSubalgebra, coe_inf, coe_top, fourierSubalgebra_closure_eq_top, coe_iInf, mem_sInf, StarAlgHom.range_eq_map_top, mem_sup_right, ContinuousMap.elemental_id_eq_top, mem_inf, ContinuousMap.starSubalgebra_topologicalClosure_eq_top_of_separatesPoints, map_iInf, iInf_toSubalgebra, top_toSubalgebra
|
copy 📖 | CompOp | 2 mathmath: coe_copy, copy_eq
|
inclusion 📖 | CompOp | 5 mathmath: inclusion_apply, subtype_comp_inclusion, isClosedEmbedding_inclusion, inclusion_injective, isEmbedding_inclusion
|
inhabited 📖 | CompOp | — |
instPartialOrder 📖 | CompOp | 22 mathmath: Subalgebra.starClosure_le, topologicalClosure_map_le, polynomialFunctions.starClosure_le_equalizer, StarAlgebra.elemental.le_of_mem, StarAlgebra.elemental.le_iff_mem, gc_map_comap, Subalgebra.starClosure_le_iff, StarAlgHom.adjoin_le_equalizer, StarAlgebra.elemental.le_centralizer_centralizer, StarAlgebra.adjoin_le_centralizer_centralizer, topologicalClosure_mono, toSubalgebra_le_iff, StarAlgebra.gc, topologicalClosure_adjoin_le_centralizer_centralizer, centralizer_le, StarAlgebra.adjoin_le_iff, map_le_iff_le_comap, StarAlgebra.adjoin_le, map_topologicalClosure_le, StarAlgebra.adjoin_mono, Unitization.starLift_range_le, le_topologicalClosure
|
map 📖 | CompOp | 19 mathmath: map_inf, coe_map, map_map, topologicalClosure_map_le, gc_map_comap, map_toSubalgebra, topologicalClosure_map, map_injective, map_sup, map_le_iff_le_comap, StarAlgHom.range_eq_map_top, map_topologicalClosure_le, mem_map, StarAlgHom.map_adjoin, map_iInf, map_id, BoundedContinuousFunction.separatesPoints_charPoly, map_mono, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict
|
ofClass 📖 | CompOp | 1 mathmath: ofClass_carrier
|
setLike 📖 | CompOp | 90 mathmath: mem_toSubalgebra, coe_sInf, StarAlgEquiv.ofInjective_symm_apply, StarAlgHom.mem_equalizer, inclusion_apply, coe_map, range_le, smulMemClass, StarAlgebra.elemental.characterSpaceToSpectrum_coe, subringClass, StarAlgebra.adjoin_eq, NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe, subtype_comp_inclusion, ofClass_carrier, StarAlgEquiv.ofInjective_apply, StarAlgebra.self_mem_adjoin_singleton, subsemiringClass, StarAlgebra.elemental.isClosed, mem_bot, mem_comap, BoundedContinuousFunction.mem_charPoly, StarAlgebra.elemental.le_iff_mem, subtype_apply, ext_iff, StarAlgebra.elemental.bijective_characterSpaceToSpectrum, isClosedEmbedding_inclusion, instIsTopologicalSemiringSubtypeMem, Subalgebra.mem_starClosure, VonNeumannAlgebra.coe_mk, eq_top_iff, VonNeumannAlgebra.mem_carrier, topologicalClosure_coe, spectrum_eq, ContinuousMap.adjoin_id_eq_span_one_union, coe_subtype, StarAlgebra.star_self_mem_adjoin_singleton, coe_bot, StarAlgebra.star_subset_adjoin, StarAlgebra.subset_adjoin, isClosed_topologicalClosure, StarAlgebra.elemental.le_centralizer_centralizer, StarAlgebra.elemental.instCompleteSpaceSubtypeMemStarSubalgebra, StarAlgebra.elemental.star_self_mem, mem_iInf, range_cfc_eq_range_cfcHom, StarAlgebra.adjoin_le_centralizer_centralizer, algebraMap_mem, mem_carrier, coe_mk, range_cfc_nnreal, mem_top, range_subset, StarAlgebra.elemental.self_mem, cfc_apply_mem_elemental, StarAlgebra.gc, starModule, topologicalClosure_adjoin_le_centralizer_centralizer, mem_spectrum_iff, coe_centralizer_centralizer, StarAlgebra.adjoin_le_iff, to_cstarRing, StarAlgebra.elemental.isClosedEmbedding_coe, coe_comap, toSubalgebra_subtype, ContinuousMap.adjoin_id_eq_span_one_add, mem_centralizer_iff, coe_inf, Subalgebra.coe_starClosure, VonNeumannAlgebra.coe_toStarSubalgebra, coe_isUnit, coe_top, coe_iInf, mem_sInf, instCanLiftSetCoeAndForallForallForallMemForallHAddForallForallForallForallHMulForallCoeRingHomAlgebraMapForallForallStar, coe_centralizer, inclusion_injective, ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id, mem_inf, coe_toSubalgebra, StarAlgebra.elemental.continuous_characterSpaceToSpectrum, mem_map, cfcHom_eq_of_isStarNormal, range_cfc, starMemClass, isEmbedding_inclusion, continuousFunctionalCalculus_map_id, StarAlgebra.mem_adjoin_of_mem, cfcHom_apply_mem_elemental, instCompleteSpaceSubtypeMemTopologicalClosure, BoundedContinuousFunction.char_mem_charPoly
|
starRing 📖 | CompOp | 1 mathmath: to_cstarRing
|
subtype 📖 | CompOp | 6 mathmath: subtype_comp_inclusion, subtype_apply, coe_subtype, toSubalgebra_subtype, StarAlgHom.subtype_comp_codRestrict, cfcHom_eq_of_isStarNormal
|
toNonUnitalStarSubalgebra 📖 | CompOp | 5 mathmath: toNonUnitalStarSubalgebra_toStarSubalgebra, NonUnitalStarSubalgebra.toStarSubalgebra_toNonUnitalStarSubalgebra, one_mem_toNonUnitalStarSubalgebra, Unitization.starLift_range_le, NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin
|
toSubalgebra 📖 | CompOp | 30 mathmath: mem_toSubalgebra, inf_toSubalgebra, UnitAddTorus.mFourierSubalgebra_coe, bot_toSubalgebra, toNonUnitalStarSubalgebra_toStarSubalgebra, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, VonNeumannAlgebra.centralizer_centralizer', fourierSubalgebra_separatesPoints, centralizer_toSubalgebra, Subalgebra.starClosure_le_iff, map_toSubalgebra, toSubalgebra_injective, Subalgebra.starClosure_toSubalgebra, rangeS_le, mem_carrier, fourierSubalgebra_coe, toSubalgebra_le_iff, toSubalgebra_eq_top, UnitAddTorus.mFourierSubalgebra_separatesPoints, StarAlgebra.adjoin_toSubalgebra, toSubalgebra_subtype, toSubalgebra_inj, sInf_toSubalgebra, StarAlgebra.adjoin_eq_span, coe_toSubalgebra, BoundedContinuousFunction.separatesPoints_charPoly, iInf_toSubalgebra, topologicalClosure_toSubalgebra_comm, top_toSubalgebra, RCLike.restrict_toContinuousMap_eq_toContinuousMapStar_restrict
|