StarAlgHom

📁 Source: Mathlib/Algebra/Star/StarAlgHom.lean

Statistics

Metric	Count
Definitions `NonUnitalAlgEquivClass`, `NonUnitalStarAlgHom`, `comp`, `copy`, `fst`, `id`, `inl`, `inr`, `instFunLike`, `instInhabited`, `instMonoid`, `instMonoidWithZero`, `instZero`, `prod`, `prodEquiv`, `restrictScalars`, `snd`, `toNonUnitalAlgHom`, `instCoeTCNonUnitalStarAlgHomOfStarHomClass`, `toNonUnitalStarAlgHom`, `evalNonUnitalStarAlgHom`, `evalStarAlgHom`, `StarAlgEquiv`, `symm_apply`, `aut`, `instEquivLike`, `instFunLike`, `instInhabited`, `ofAlgEquiv`, `ofBijective`, `ofStarAlgHom`, `refl`, `aux`, `toAlgEquiv`, `toStarRingEquiv`, `trans`, `instCoeHead`, `toStarAlgEquiv`, `StarAlgHom`, `comp`, `copy`, `fst`, `id`, `instFunLike`, `instInhabited`, `instMonoid`, `ofId`, `prod`, `prodEquiv`, `snd`, `toAlgHom`, `toNonUnitalStarAlgHom`, `instCoeTCStarAlgHom`, `toStarAlgHom`, `«term_→⋆ₐ[_]_»`, `«term_→⋆ₐ_»`, `«term_→⋆ₙₐ[_]_»`, `«term_→⋆ₙₐ_»`, `«term_≃⋆ₐ[_]_»`, `«term_≃⋆ₐ_»`	60
Theorems `toMulActionSemiHomClass`, `toRingEquivClass`, `coe_coe`, `coe_comp`, `coe_copy`, `coe_id`, `coe_inl`, `coe_inr`, `coe_mk`, `coe_mk'`, `coe_one`, `coe_prod`, `coe_restrictScalars`, `coe_restrictScalars'`, `coe_toNonUnitalAlgHom`, `coe_zero`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `ext`, `ext_iff`, `fst_apply`, `fst_prod`, `id_comp`, `inl_apply`, `inr_apply`, `instNonUnitalAlgHomClass`, `instStarHomClass`, `map_star'`, `mk_coe`, `one_apply`, `prodEquiv_apply`, `prodEquiv_symm_apply`, `prod_apply`, `prod_fst_snd`, `restrictScalars_apply`, `restrictScalars_injective`, `snd_apply`, `snd_prod`, `zero_apply`, `instNonUnitalStarRingHomClassOfStarHomClass`, `evalNonUnitalStarAlgHom_apply`, `evalStarAlgHom_apply`, `apply_symm_apply`, `aut_inv`, `aut_mul`, `aut_one`, `coe_mk`, `coe_ofBijective`, `coe_pow`, `coe_refl`, `coe_symm_toAlgEquiv`, `coe_toAlgEquiv`, `coe_trans`, `ext`, `ext_iff`, `instNonUnitalAlgEquivClass`, `instStarRingEquivClass`, `invFun_eq_symm`, `leftInverse_symm`, `map_smul'`, `mk_coe`, `mul_apply`, `ofAlgEquiv_apply`, `ofAlgEquiv_symm`, `ofAlgEquiv_toAlgEquiv`, `ofBijective_apply`, `ofStarAlgHom_apply`, `ofStarAlgHom_symm_apply`, `one_apply`, `refl_symm`, `rightInverse_symm`, `symm_apply_apply`, `symm_bijective`, `symm_mk`, `symm_symm`, `symm_to_ringEquiv`, `symm_trans_apply`, `toAlgEquiv_injective`, `toAlgEquiv_ofAlgEquiv`, `toAlgEquiv_refl`, `toAlgEquiv_symm`, `toAlgEquiv_trans`, `toRingEquiv_eq_coe`, `toRingEquiv_symm`, `toStarRingEquiv_eq_coe`, `toStarRingEquiv_symm`, `to_ringEquiv_symm`, `trans_apply`, `coe_coe`, `coe_comp`, `coe_copy`, `coe_id`, `coe_mk`, `coe_mk'`, `coe_prod`, `coe_toAlgHom`, `coe_toNonUnitalStarAlgHom`, `comp_apply`, `comp_assoc`, `comp_id`, `copy_eq`, `ext`, `ext_iff`, `fst_apply`, `fst_prod`, `id_comp`, `instAlgHomClass`, `instStarHomClass`, `map_star'`, `mk_coe`, `ofId_apply`, `prodEquiv_apply`, `prodEquiv_symm_apply`, `prod_apply`, `prod_fst_snd`, `snd_apply`, `snd_prod`, `instAlgEquivClassOfNonUnitalAlgEquivClass`, `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass`	121
Total	181

NonUnitalAlgEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`toMulActionSemiHomClass` 📖	mathematical	—	`MulActionSemiHomClass` `EquivLike.toFunLike`	—	—
`toRingEquivClass` 📖	mathematical	—	`RingEquivClass`	—	—

NonUnitalStarAlgHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	16 math math: `id_comp`, `Unitization.starAlgHom_ext_iff`, `prodEquiv_symm_apply`, `coe_comp`, `comp_assoc`, `range_comp_le_range`, `NonUnitalStarSubalgebra.map_map`, `comp_apply`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `comp_id`, `Unitization.starMap_comp`, `fst_prod`, `subtype_comp_codRestrict`, `snd_prod`, `Unitization.starLift_symm_apply`, `range_comp`
`copy` 📖	CompOp	2 math math: `copy_eq`, `coe_copy`
`fst` 📖	CompOp	4 math math: `prodEquiv_symm_apply`, `prod_fst_snd`, `fst_apply`, `fst_prod`
`id` 📖	CompOp	6 math math: `id_comp`, `Unitization.starMap_id`, `comp_id`, `NonUnitalStarAlgebra.range_id`, `coe_id`, `NonUnitalStarSubalgebra.map_id`
`inl` 📖	CompOp	2 math math: `inl_apply`, `coe_inl`
`inr` 📖	CompOp	2 math math: `inr_apply`, `coe_inr`
`instFunLike` 📖	CompOp	104 math math: `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `norm_cfcₙHom`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `coe_codRestrict`, `inl_apply`, `isClosedEmbedding_cfcₙAux`, `coe_restrictScalars`, `realContinuousMapZeroOfNNReal_apply_comp_toReal`, `coe_comp`, `Unitization.starLift_symm_apply_apply`, `Unitization.starLift_apply_apply`, `range_comp_le_range`, `instStarHomClass`, `injective_codRestrict`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `range_cfcₙHom`, `NonUnitalStarSubalgebra.map_map`, `PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe`, `NonUnitalStarSubalgebra.val_inclusion`, `cfcₙHom_integral`, `comp_apply`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `Unitization.starLift_range`, `prod_apply`, `inr_apply`, `Unitization.inrNonUnitalStarAlgHom_apply`, `NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype`, `NonUnitalStarSubalgebra.range_val`, `Commute.cfcₙHom`, `Unitization.starMap_inr`, `NonUnitalStarSubalgebra.inclusion_mk`, `range_cfcₙ_eq_range_cfcₙHom`, `NonUnitalStarSubalgebraClass.coe_subtype`, `restrictScalars_apply`, `ContinuousMapZero.nonUnitalStarAlgHom_precomp_apply`, `NonUnitalStarSubalgebra.iSupLift_inclusion`, `coe_toNonUnitalAlgHom`, `coe_restrictScalars'`, `snd_apply`, `coe_zero`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `realContinuousMapZeroOfNNReal_apply`, `coe_one`, `cfcₙHom_eq_cfcₙ_extend`, `fst_apply`, `ContinuousMapZero.toContinuousMapHom_toNNReal`, `NonUnitalStarSubalgebra.iSupLift_of_mem`, `DoubleCentralizer.coeHom_apply`, `cfcₙHom_map_quasispectrum`, `spec_cfcₙAux`, `coe_coe`, `cfcₙHomSuperset_id`, `nnnorm_cfcₙHom`, `NonUnitalStarSubalgebra.inclusion_right`, `NonUnitalStarSubalgebraClass.subtype_injective`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `Unitization.starMap_apply`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `StarAlgHom.coe_toNonUnitalStarAlgHom`, `ContinuousMapZero.toContinuousMapHom_apply`, `NonUnitalStarSubalgebra.toSubring_subtype`, `cfcₙAux_mem_range_inr`, `Pi.evalNonUnitalStarAlgHom_apply`, `one_apply`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `cfcₙ_apply_pi`, `coe_prod`, `Unitization.inrRangeEquiv_apply_coe`, `NonUnitalStarAlgebra.range_id`, `coe_mk'`, `NonUnitalStarSubalgebra.inclusion_injective`, `cfcₙL_apply`, `coe_inr`, `Unitization.starLift_range_le`, `coe_mk`, `coe_inl`, `ext_iff`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `coe_id`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `ContinuousMapZero.coe_toContinuousMapHom`, `NonUnitalStarSubalgebraClass.subtype_apply`, `Unitization.inrRangeEquiv_symm_apply`, `NonUnitalStarSubalgebra.iSupLift_mk`, `cfcₙHom_nonneg_iff`, `CStarMatrix.mapₙₐ_apply`, `PositiveLinearMap.gnsNonUnitalStarAlgHom_apply`, `NonUnitalStarSubalgebra.inclusion_self`, `NonUnitalStarSubalgebra.map_id`, `zero_apply`, `NonUnitalStarSubalgebra.inclusion_inclusion`, `instNonUnitalAlgHomClass`, `range_comp`
`instInhabited` 📖	CompOp	—
`instMonoid` 📖	CompOp	3 math math: `prod_fst_snd`, `coe_one`, `one_apply`
`instMonoidWithZero` 📖	CompOp	—
`instZero` 📖	CompOp	2 math math: `coe_zero`, `zero_apply`
`prod` 📖	CompOp	6 math math: `prod_fst_snd`, `prod_apply`, `prodEquiv_apply`, `fst_prod`, `coe_prod`, `snd_prod`
`prodEquiv` 📖	CompOp	2 math math: `prodEquiv_symm_apply`, `prodEquiv_apply`
`restrictScalars` 📖	CompOp	4 math math: `coe_restrictScalars`, `restrictScalars_injective`, `restrictScalars_apply`, `coe_restrictScalars'`
`snd` 📖	CompOp	4 math math: `prodEquiv_symm_apply`, `prod_fst_snd`, `snd_apply`, `snd_prod`
`toNonUnitalAlgHom` 📖	CompOp	5 math math: `coe_toNonUnitalAlgHom`, `PositiveLinearMap.gnsStarAlgHom_apply`, `Unitization.starLift_apply`, `Pi.evalStarAlgHom_apply`, `map_star'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `NonUnitalStarAlgHomClass.toNonUnitalStarAlgHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `id`	—	—
`coe_inl` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `Prod.instStar` `instFunLike` `inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`coe_inr` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `Prod.instStar` `instFunLike` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`coe_mk` 📖	mathematical	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `MonoidHom.id` `MulActionHom.toFun` `AddZero.toAdd` `DistribMulActionHom.toMulActionHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalAlgHom.toDistribMulActionHom` `Star.star`	`NonUnitalStarAlgHom` `instFunLike`	—	—
`coe_mk'` 📖	mathematical	`MulActionHom.toFun` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `MonoidHom.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DistribMulActionHom.toMulActionHom` `NonUnitalAlgHom.toDistribMulActionHom` `Star.star`	`NonUnitalStarAlgHom` `instFunLike` `NonUnitalAlgHom` `NonUnitalAlgHom.instFunLike_1`	—	—
`coe_one` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `instFunLike` `prod` `Pi.prod`	—	—
`coe_restrictScalars` 📖	mathematical	—	`NonUnitalRingHomClass.toNonUnitalRingHom` `NonUnitalStarAlgHom` `instFunLike` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instNonUnitalAlgHomClass` `restrictScalars`	—	`NonUnitalAlgHomClass.toNonUnitalRingHomClass` `instNonUnitalAlgHomClass`
`coe_restrictScalars'` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `restrictScalars`	—	—
`coe_toNonUnitalAlgHom` 📖	mathematical	—	`DFunLike.coe` `NonUnitalAlgHom` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `NonUnitalAlgHom.instFunLike_1` `toNonUnitalAlgHom` `NonUnitalStarAlgHom` `instFunLike`	—	—
`coe_zero` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instZero` `Pi.instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike`	—	`ext`
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `instFunLike` `fst`	—	—
`fst_prod` 📖	mathematical	—	`comp` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `fst` `prod`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `Prod.instStar` `instFunLike` `inl` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `Prod.instStar` `instFunLike` `inr` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—
`instNonUnitalAlgHomClass` 📖	mathematical	—	`NonUnitalAlgHomClass` `NonUnitalStarAlgHom` `instFunLike`	—	`MulActionHom.map_smul'` `DistribMulActionHom.map_add'` `DistribMulActionHom.map_zero'` `NonUnitalAlgHom.map_mul'`
`instStarHomClass` 📖	mathematical	—	`StarHomClass` `NonUnitalStarAlgHom` `instFunLike`	—	`map_star'`
`map_star'` 📖	mathematical	—	`MulActionHom.toFun` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `MonoidHom.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `DistribMulActionHom.toMulActionHom` `NonUnitalAlgHom.toDistribMulActionHom` `toNonUnitalAlgHom` `Star.star`	—	—
`mk_coe` 📖	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidHom.instFunLike` `MonoidHom.id` `MulActionHom.toFun` `AddZero.toAdd` `DistribMulActionHom.toMulActionHom` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalAlgHom.toDistribMulActionHom` `Star.star`	—	—	`ext`
`one_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	—
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonUnitalStarAlgHom` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `prod`	—	—
`prodEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `NonUnitalStarAlgHom` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodEquiv` `comp` `fst` `snd`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `instFunLike` `prod`	—	—
`prod_fst_snd` 📖	mathematical	—	`prod` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `fst` `snd` `NonUnitalStarAlgHom` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	`DFunLike.coe_injective` `Pi.prod_fst_snd`
`restrictScalars_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `instFunLike` `restrictScalars`	—	—
`restrictScalars_injective` 📖	mathematical	—	`NonUnitalStarAlgHom` `restrictScalars`	—	`ext` `DFunLike.congr_fun`
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `instFunLike` `snd`	—	—
`snd_prod` 📖	mathematical	—	`comp` `Prod.instNonUnitalNonAssocSemiring` `Prod.distribMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Prod.instStar` `snd` `prod`	—	`ext`
`zero_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `instFunLike` `instZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	—

NonUnitalStarAlgHomClass

Definitions

Name	Category	Theorems
`instCoeTCNonUnitalStarAlgHomOfStarHomClass` 📖	CompOp	—
`toNonUnitalStarAlgHom` 📖	CompOp	4 math math: `Unitization.starAlgHom_ext_iff`, `NonUnitalStarAlgHom.coe_coe`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `NonUnitalStarAlgHom.subtype_comp_codRestrict`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instNonUnitalStarRingHomClassOfStarHomClass` 📖	mathematical	—	`NonUnitalStarRingHomClass` `NonUnitalAlgHomClass.toNonUnitalRingHomClass` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`NonUnitalAlgHomClass.toNonUnitalRingHomClass`

Pi

Definitions

Name	Category	Theorems
`evalNonUnitalStarAlgHom` 📖	CompOp	2 math math: `evalNonUnitalStarAlgHom_apply`, `evalStarAlgHom_apply`
`evalStarAlgHom` 📖	CompOp	1 math math: `evalStarAlgHom_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`evalNonUnitalStarAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `nonUnitalNonAssocSemiring` `distribMulAction` `AddCommMonoid.toAddMonoid` `instStarForall` `NonUnitalStarAlgHom.instFunLike` `evalNonUnitalStarAlgHom` `MulHom.toFun` `instMul` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `evalMulHom`	—	—
`evalStarAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `semiring` `algebra` `instStarForall` `StarAlgHom.instFunLike` `evalStarAlgHom` `MulActionHom.toFun` `MonoidHom` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `MonoidHom.instFunLike` `MonoidHom.id` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `nonUnitalNonAssocSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `distribMulAction` `Module.toDistribMulAction` `Algebra.toModule` `DistribMulActionHom.toMulActionHom` `NonUnitalAlgHom.toDistribMulActionHom` `NonUnitalStarAlgHom.toNonUnitalAlgHom` `evalNonUnitalStarAlgHom`	—	—

StarAlgEquiv

Definitions

Name	Category	Theorems
`aut` 📖	CompOp	22 math math: `Unitary.conjStarAlgAut_trans_conjStarAlgAut`, `Unitary.conjStarAlgAut_symm`, `Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv`, `mul_apply`, `aut_mul`, `one_apply`, `aut_inv`, `Unitary.conjStarAlgAut_ext_iff'`, `Matrix.IsHermitian.cfcAux_apply`, `Unitary.conjStarAlgAut_apply`, `Unitary.toAlgEquiv_conjStarAlgAut`, `coe_pow`, `Unitary.conjStarAlgAut_symm_apply`, `Unitary.toRingEquiv_conjStarAlgAut`, `Matrix.IsHermitian.spectral_theorem`, `Unitary.conjStarAlgAut_mul_apply`, `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal`, `Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv`, `aut_one`, `Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `Unitary.conjStarAlgAut_star_apply`, `Unitary.conjStarAlgAut_ext_iff`
`instEquivLike` 📖	CompOp	11 math math: `toStarRingEquiv_symm`, `gelfandStarTransform_naturality`, `toStarRingEquiv_eq_coe`, `toRingEquiv_symm`, `symm_to_ringEquiv`, `toRingEquiv_eq_coe`, `instStarRingEquivClass`, `to_ringEquiv_symm`, `cfcHom_eq_of_isStarNormal`, `instNonUnitalAlgEquivClass`, `invFun_eq_symm`
`instFunLike` 📖	CompOp	66 math math: `Matrix.l2_opNorm_toEuclideanCLM`, `ofInjective_symm_apply`, `Matrix.kroneckerTMulStarAlgEquiv_symm_apply`, `ofLeftInverse'_apply`, `ofStarAlgHom_symm_apply`, `Matrix.cstar_nnnorm_def`, `mul_apply`, `CStarMatrix.mapₗ_reindexₐ`, `ofStarAlgHom_apply`, `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `LinearIsometryEquiv.conjStarAlgEquiv_apply`, `restrictScalars_symm_apply`, `LinearMap.toMatrixOrthonormal_reindex`, `coe_toAlgEquiv`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `ofInjective_apply`, `LinearMap.toMatrixOrthonormal_apply_apply`, `coe_refl`, `one_apply`, `gelfandStarTransform_symm_apply`, `Matrix.toEuclideanCLM_toLp`, `rightInverse_symm`, `leftInverse_symm`, `LinearMap.toMatrixOrthonormal_symm_apply`, `ofBijective_apply`, `Matrix.IsHermitian.cfcAux_apply`, `Matrix.ofLp_toEuclideanCLM`, `coe_ofBijective`, `Matrix.kroneckerTMulStarAlgEquiv_apply`, `apply_symm_apply`, `CStarMatrix.reindexₐ_apply`, `Unitary.conjStarAlgAut_apply`, `coe_pow`, `Matrix.coe_toEuclideanCLM_eq_toEuclideanLin`, `LinearMap.toMatrixOrthonormal_apply`, `Unitary.conjStarAlgAut_symm_apply`, `coe_symm_toAlgEquiv`, `symm_apply_apply`, `Matrix.IsHermitian.spectral_theorem`, `LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply`, `coe_trans`, `restrictScalars_apply`, `CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv`, `symm_trans_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `Unitary.conjStarAlgAut_mul_apply`, `ext_iff`, `ofAlgEquiv_apply`, `Unitization.inrRangeEquiv_apply_coe`, `ofInjective'_apply`, `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `Matrix.cstar_norm_def`, `coe_mk`, `ofLeftInverse'_symm_apply`, `Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `cfcHom_eq_of_isStarNormal`, `Unitary.conjStarAlgAut_star_apply`, `Matrix.kroneckerStarAlgEquiv_apply`, `Unitization.inrRangeEquiv_symm_apply`, `trans_apply`, `LinearIsometryEquiv.conjStarAlgEquiv_apply_apply`, `continuousFunctionalCalculus_map_id`, `invFun_eq_symm`, `Matrix.kroneckerStarAlgEquiv_symm_apply`
`instInhabited` 📖	CompOp	—
`ofAlgEquiv` 📖	CompOp	4 math math: `toAlgEquiv_ofAlgEquiv`, `ofAlgEquiv_toAlgEquiv`, `ofAlgEquiv_apply`, `ofAlgEquiv_symm`
`ofBijective` 📖	CompOp	2 math math: `ofBijective_apply`, `coe_ofBijective`
`ofStarAlgHom` 📖	CompOp	2 math math: `ofStarAlgHom_symm_apply`, `ofStarAlgHom_apply`
`refl` 📖	CompOp	5 math math: `coe_refl`, `toAlgEquiv_refl`, `LinearIsometryEquiv.conjStarAlgEquiv_refl`, `refl_symm`, `aut_one`
`toAlgEquiv` 📖	CompOp	10 math math: `coe_toAlgEquiv`, `toAlgEquiv_injective`, `Matrix.toAlgEquiv_kroneckerStarAlgEquiv`, `Matrix.toAlgEquiv_kroneckerTMulStarAlgEquiv`, `toAlgEquiv_symm`, `toAlgEquiv_refl`, `toAlgEquiv_ofAlgEquiv`, `Unitary.toAlgEquiv_conjStarAlgAut`, `toAlgEquiv_trans`, `coe_symm_toAlgEquiv`
`toStarRingEquiv` 📖	CompOp	6 math math: `restrictScalars_symm_apply`, `toStarRingEquiv_eq_coe`, `toRingEquiv_eq_coe`, `Unitary.toRingEquiv_conjStarAlgAut`, `map_smul'`, `ofAlgEquiv_symm`
`trans` 📖	CompOp	7 math math: `Unitary.conjStarAlgAut_trans_conjStarAlgAut`, `aut_mul`, `LinearIsometryEquiv.conjStarAlgEquiv_trans`, `toAlgEquiv_trans`, `coe_trans`, `symm_trans_apply`, `trans_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_symm_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `symm`	—	`StarRingEquiv.apply_symm_apply`
`aut_inv` 📖	mathematical	—	`StarAlgEquiv` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `aut` `symm`	—	—
`aut_mul` 📖	mathematical	—	`StarAlgEquiv` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `aut` `trans`	—	—
`aut_one` 📖	mathematical	—	`StarAlgEquiv` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `aut` `refl`	—	—
`coe_mk` 📖	mathematical	`Equiv.toFun` `RingEquiv.toEquiv` `StarRingEquiv.toRingEquiv`	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `StarRingEquiv` `StarRingEquiv.instFunLike`	—	—
`coe_ofBijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe`	`StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instFunLike` `ofBijective`	—	—
`coe_pow` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `aut` `Nat.iterate`	—	`hom_coe_pow` `one_apply` `mul_apply`
`coe_refl` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `refl`	—	—
`coe_symm_toAlgEquiv` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `AlgEquiv.symm` `toAlgEquiv` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `instFunLike` `symm`	—	—
`coe_toAlgEquiv` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `toAlgEquiv` `StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `instFunLike`	—	—
`coe_trans` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `trans`	—	—
`ext` 📖	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike`	—	`ext`
`instNonUnitalAlgEquivClass` 📖	mathematical	—	`NonUnitalAlgEquivClass` `StarAlgEquiv` `instEquivLike`	—	`RingEquiv.map_mul'` `RingEquiv.map_add'` `map_smul'`
`instStarRingEquivClass` 📖	mathematical	—	`StarRingEquivClass` `StarAlgEquiv` `instEquivLike`	—	`NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `StarRingEquiv.map_star'`
`invFun_eq_symm` 📖	mathematical	—	`EquivLike.inv` `StarAlgEquiv` `instEquivLike` `DFunLike.coe` `instFunLike` `symm`	—	—
`leftInverse_symm` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `symm`	—	`Equiv.left_inv`
`map_smul'` 📖	mathematical	—	`Equiv.toFun` `RingEquiv.toEquiv` `StarRingEquiv.toRingEquiv` `toStarRingEquiv`	—	—
`mk_coe` 📖	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `Equiv.toFun` `RingEquiv.toEquiv` `Star.star` `StarRingEquiv.toRingEquiv`	—	—	`ext`
`mul_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `aut`	—	—
`ofAlgEquiv_apply` 📖	mathematical	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `Star.star`	`StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `instFunLike` `ofAlgEquiv`	—	—
`ofAlgEquiv_symm` 📖	mathematical	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `Star.star`	`symm` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `ofAlgEquiv` `AlgEquiv.symm` `StarRingEquiv.map_star'` `toStarRingEquiv`	—	—
`ofAlgEquiv_toAlgEquiv` 📖	mathematical	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `toAlgEquiv` `Star.star`	`ofAlgEquiv`	—	—
`ofBijective_apply` 📖	mathematical	`Function.Bijective` `DFunLike.coe`	`StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instFunLike` `ofBijective`	—	—
`ofStarAlgHom_apply` 📖	mathematical	`DFunLike.coe`	`StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instFunLike` `ofStarAlgHom`	—	—
`ofStarAlgHom_symm_apply` 📖	mathematical	`DFunLike.coe`	`StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `Distrib.toMul` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `instFunLike` `symm` `ofStarAlgHom`	—	—
`one_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid` `aut`	—	—
`refl_symm` 📖	mathematical	—	`symm` `refl`	—	—
`rightInverse_symm` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `symm`	—	`Equiv.right_inv`
`symm_apply_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `symm`	—	`StarRingEquiv.symm_apply_apply`
`symm_bijective` 📖	mathematical	—	`Function.Bijective` `StarAlgEquiv` `symm`	—	`Function.bijective_iff_has_inverse` `symm_symm`
`symm_mk` 📖	mathematical	`Equiv.toFun` `RingEquiv.toEquiv` `Star.star` `StarRingEquiv.toRingEquiv`	`symm`	—	—
`symm_symm` 📖	mathematical	—	`symm`	—	—
`symm_to_ringEquiv` 📖	mathematical	—	`RingEquivClass.toRingEquiv` `StarAlgEquiv` `instEquivLike` `NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `symm` `RingEquiv.symm`	—	`toRingEquiv_symm`
`symm_trans_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `symm` `trans`	—	—
`toAlgEquiv_injective` 📖	mathematical	—	`StarAlgEquiv` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `AlgEquiv` `toAlgEquiv`	—	`ext` `AlgEquiv.congr_fun`
`toAlgEquiv_ofAlgEquiv` 📖	mathematical	`DFunLike.coe` `AlgEquiv` `AlgEquiv.instFunLike` `Star.star`	`toAlgEquiv` `ofAlgEquiv`	—	—
`toAlgEquiv_refl` 📖	mathematical	—	`toAlgEquiv` `refl` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `AlgEquiv.refl`	—	—
`toAlgEquiv_symm` 📖	mathematical	—	`toAlgEquiv` `symm` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `AlgEquiv.symm`	—	—
`toAlgEquiv_trans` 📖	mathematical	—	`toAlgEquiv` `trans` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `Algebra.toSMul` `AlgEquiv.trans`	—	—
`toRingEquiv_eq_coe` 📖	mathematical	—	`StarRingEquiv.toRingEquiv` `toStarRingEquiv` `RingEquivClass.toRingEquiv` `StarAlgEquiv` `instEquivLike` `NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass`	—	—
`toRingEquiv_symm` 📖	mathematical	—	`RingEquivClass.toRingEquiv` `StarAlgEquiv` `instEquivLike` `NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `symm` `RingEquiv.symm`	—	`NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass`
`toStarRingEquiv_eq_coe` 📖	mathematical	—	`toStarRingEquiv` `StarRingEquivClass.toStarRingEquiv` `StarAlgEquiv` `instEquivLike` `NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `instStarRingEquivClass`	—	—
`toStarRingEquiv_symm` 📖	mathematical	—	`StarRingEquivClass.toStarRingEquiv` `StarAlgEquiv` `instEquivLike` `NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `instStarRingEquivClass` `symm` `StarRingEquiv.symm`	—	`NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `instStarRingEquivClass`
`to_ringEquiv_symm` 📖	mathematical	—	`RingEquiv.symm` `RingEquivClass.toRingEquiv` `StarAlgEquiv` `instEquivLike` `NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass` `symm`	—	`NonUnitalAlgEquivClass.toRingEquivClass` `instNonUnitalAlgEquivClass`
`trans_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgEquiv` `instFunLike` `trans`	—	—

StarAlgEquiv.Simps

Definitions

Name	Category	Theorems
`symm_apply` 📖	CompOp	—

StarAlgEquiv.symm_mk

Definitions

Name	Category	Theorems
`aux` 📖	CompOp	—

StarAlgEquivClass

Definitions

Name	Category	Theorems
`instCoeHead` 📖	CompOp	—
`toStarAlgEquiv` 📖	CompOp	—

StarAlgHom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	18 math math: `comp_assoc`, `StarSubalgebra.subtype_comp_inclusion`, `gelfandStarTransform_naturality`, `StarSubalgebra.map_map`, `comp_apply`, `ContinuousMap.compStarAlgHom_comp`, `ContinuousMap.compStarAlgHom'_comp`, `snd_prod`, `id_comp`, `coe_comp`, `StarSubalgebra.comap_comap`, `comp_id`, `Unitization.starMap_comp`, `subtype_comp_codRestrict`, `prodEquiv_symm_apply`, `fst_prod`, `WeakDual.CharacterSpace.compContinuousMap_comp`, `cfcHom_eq_of_isStarNormal`
`copy` 📖	CompOp	2 math math: `coe_copy`, `copy_eq`
`fst` 📖	CompOp	4 math math: `prod_fst_snd`, `prodEquiv_symm_apply`, `fst_prod`, `fst_apply`
`id` 📖	CompOp	9 math math: `Unitization.starMap_id`, `id_comp`, `StarSubalgebra.comap_id`, `comp_id`, `ContinuousMap.compStarAlgHom_id`, `ContinuousMap.compStarAlgHom'_id`, `coe_id`, `WeakDual.CharacterSpace.compContinuousMap_id`, `StarSubalgebra.map_id`
`instFunLike` 📖	CompOp	85 math math: `Matrix.IsHermitian.isClosedEmbedding_cfcAux`, `IsSelfAdjoint.commute_cfcHom`, `StarSubalgebra.inclusion_apply`, `StarSubalgebra.coe_map`, `Unitization.starAlgHom_ext_iff`, `cfcHom_continuous`, `cfcL_apply`, `snd_apply`, `cfcHom_nonneg_iff`, `cfc_apply_mkD`, `coe_prod`, `Unitization.starLift_symm_apply_apply`, `Unitization.starLift_apply_apply`, `cfcHom_isClosedEmbedding`, `BoundedContinuousFunction.coe_toContinuousMapStarₐ`, `comp_apply`, `cfcHom_le_iff`, `cfcHom_id`, `StarSubalgebra.mem_comap`, `coe_mk'`, `coe_mk`, `realContinuousMapOfNNReal_apply`, `gelfandStarTransform_symm_apply`, `StarSubalgebra.subtype_apply`, `Unitization.starMap_injective`, `instStarHomClass`, `ext_iff`, `coe_coe`, `StarSubalgebra.isClosedEmbedding_inclusion`, `cfcHom_integral`, `ContinuousFunctionalCalculus.exists_cfc_of_predicate`, `coe_toAlgHom`, `restrictScalars_apply`, `cfc_def`, `Unitization.starMap_inl`, `realContinuousMapOfNNReal_apply_comp_toReal`, `Unitization.starMap_inr`, `NonUnitalStarSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_apply`, `Unitization.starMap_surjective`, `Matrix.IsHermitian.cfcAux_apply`, `StarSubalgebra.coe_subtype`, `ofId_apply`, `continuous_cfcHomSuperset_left`, `PositiveLinearMap.gnsStarAlgHom_apply`, `cfcHomSuperset_apply`, `coe_comp`, `cfcHom_eq_cfc_extend`, `SpectrumRestricts.starAlgHom_apply`, `instAlgHomClass`, `Commute.cfcHom`, `ContinuousMap.evalStarAlgHom_apply`, `ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `cfc_apply`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `Unitization.starMap_apply`, `cfcHom_isStrictlyPositive_iff`, `coe_toNonUnitalStarAlgHom`, `BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `cfc_apply_pi`, `StarSubalgebra.coe_comap`, `Matrix.IsHermitian.cfcAux_id`, `prod_apply`, `cfcHomSuperset_id`, `StarSubalgebra.inclusion_injective`, `cfcHom_predicate`, `norm_cfcHom`, `ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id`, `cfcHomSuperset_continuous`, `ContinuousMap.compStarAlgHom'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `nnnorm_cfcHom`, `Pi.evalStarAlgHom_apply`, `ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id`, `StarSubalgebra.mem_map`, `map_adjoin`, `cfcHom_mono`, `IsometricContinuousFunctionalCalculus.isometric`, `coe_id`, `cfcHom_map_spectrum`, `StarSubalgebra.isEmbedding_inclusion`, `fst_apply`, `cfcHom_apply_mem_elemental`, `isometry_cfcHom`
`instInhabited` 📖	CompOp	—
`instMonoid` 📖	CompOp	1 math math: `prod_fst_snd`
`ofId` 📖	CompOp	3 math math: `ofId_apply`, `SpectrumRestricts.starAlgHom_apply`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`
`prod` 📖	CompOp	6 math math: `prodEquiv_apply`, `coe_prod`, `snd_prod`, `prod_fst_snd`, `prod_apply`, `fst_prod`
`prodEquiv` 📖	CompOp	2 math math: `prodEquiv_apply`, `prodEquiv_symm_apply`
`snd` 📖	CompOp	4 math math: `snd_apply`, `snd_prod`, `prod_fst_snd`, `prodEquiv_symm_apply`
`toAlgHom` 📖	CompOp	6 math math: `ContinuousMap.compStarAlgHom_comp`, `coe_toAlgHom`, `StarSubalgebra.map_toSubalgebra`, `WeakDual.CharacterSpace.compContinuousMap_apply`, `StarSubalgebra.toSubalgebra_subtype`, `map_star'`
`toNonUnitalStarAlgHom` 📖	CompOp	2 math math: `coe_toNonUnitalStarAlgHom`, `Unitization.starLift_symm_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_coe` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `instFunLike` `StarAlgHomClass.toStarAlgHom`	—	—
`coe_comp` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `instFunLike` `comp`	—	—
`coe_copy` 📖	mathematical	`DFunLike.coe` `StarAlgHom` `instFunLike`	`copy`	—	—
`coe_id` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `instFunLike` `id`	—	—
`coe_mk` 📖	mathematical	`MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `OneHom.toFun` `MulOne.toMul` `MonoidHom.toOneHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddZero.toAdd` `RingHom.toMonoidHom` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `AlgHom.toRingHom` `Star.star`	`StarAlgHom` `instFunLike`	—	—
`coe_mk'` 📖	mathematical	`OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `AlgHom.toRingHom` `Star.star`	`DFunLike.coe` `StarAlgHom` `instFunLike` `AlgHom` `AlgHom.funLike`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `instFunLike` `prod` `Pi.prod`	—	—
`coe_toAlgHom` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `toAlgHom` `StarAlgHom` `instFunLike`	—	—
`coe_toNonUnitalStarAlgHom` 📖	mathematical	—	`DFunLike.coe` `NonUnitalStarAlgHom` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Module.toDistribMulAction` `NonUnitalNonAssocSemiring.toAddCommMonoid` `Algebra.toModule` `NonUnitalStarAlgHom.instFunLike` `toNonUnitalStarAlgHom` `StarAlgHom` `instFunLike`	—	—
`comp_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `instFunLike` `comp`	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `id`	—	`ext`
`copy_eq` 📖	mathematical	`DFunLike.coe` `StarAlgHom` `instFunLike`	`copy`	—	`DFunLike.ext'`
`ext` 📖	—	`DFunLike.coe` `StarAlgHom` `instFunLike`	—	—	`DFunLike.ext`
`ext_iff` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `instFunLike`	—	`ext`
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `instFunLike` `fst`	—	—
`fst_prod` 📖	mathematical	—	`comp` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `fst` `prod`	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `id`	—	`ext`
`instAlgHomClass` 📖	mathematical	—	`AlgHomClass` `StarAlgHom` `instFunLike`	—	`MonoidHom.map_mul'` `OneHom.map_one'` `RingHom.map_add'` `RingHom.map_zero'` `AlgHom.commutes'`
`instStarHomClass` 📖	mathematical	—	`StarHomClass` `StarAlgHom` `instFunLike`	—	`map_star'`
`map_star'` 📖	mathematical	—	`OneHom.toFun` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `MonoidHom.toOneHom` `RingHom.toMonoidHom` `AlgHom.toRingHom` `toAlgHom` `Star.star`	—	—
`mk_coe` 📖	—	`DFunLike.coe` `StarAlgHom` `instFunLike` `MulOne.toOne` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring` `OneHom.toFun` `MulOne.toMul` `MonoidHom.toOneHom` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `AddZero.toAdd` `RingHom.toMonoidHom` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `AlgHom.toRingHom` `Star.star`	—	—	`ext`
`ofId_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `CommSemiring.toSemiring` `Algebra.id` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `StarMul.toInvolutiveStar` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `instFunLike` `ofId` `RingHom` `RingHom.instFunLike` `algebraMap`	—	—
`prodEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `StarAlgHom` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `prodEquiv` `prod`	—	—
`prodEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `Equiv` `StarAlgHom` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `prodEquiv` `comp` `fst` `snd`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `instFunLike` `prod`	—	—
`prod_fst_snd` 📖	mathematical	—	`prod` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `fst` `snd` `StarAlgHom` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `instMonoid`	—	`DFunLike.coe_injective` `Pi.prod_fst_snd`
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `StarAlgHom` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `instFunLike` `snd`	—	—
`snd_prod` 📖	mathematical	—	`comp` `Prod.instSemiring` `Prod.algebra` `Prod.instStar` `snd` `prod`	—	`ext`

StarAlgHomClass

Definitions

Name	Category	Theorems
`instCoeTCStarAlgHom` 📖	CompOp	—
`toStarAlgHom` 📖	CompOp	3 math math: `gelfandStarTransform_naturality`, `StarAlgHom.coe_coe`, `cfcHom_eq_of_isStarNormal`

(root)

Definitions

Name	Category	Theorems
`NonUnitalAlgEquivClass` 📖	CompData	1 math math: `StarAlgEquiv.instNonUnitalAlgEquivClass`
`NonUnitalStarAlgHom` 📖	CompData	112 math math: `cfcₙ_def`, `continuous_cfcₙHomSuperset_left`, `norm_cfcₙHom`, `cfcₙHom_mono`, `NonUnitalIsometricContinuousFunctionalCalculus.isometric`, `cfcₙHom_apply_mem_elemental`, `NonUnitalStarAlgHom.coe_codRestrict`, `NonUnitalStarAlgHom.inl_apply`, `isClosedEmbedding_cfcₙAux`, `NonUnitalStarAlgHom.coe_restrictScalars`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply_comp_toReal`, `NonUnitalStarAlgHom.prodEquiv_symm_apply`, `NonUnitalStarAlgHom.coe_comp`, `Unitization.starLift_symm_apply_apply`, `Unitization.starLift_apply_apply`, `NonUnitalStarAlgHom.range_comp_le_range`, `NonUnitalStarAlgHom.instStarHomClass`, `NonUnitalStarAlgHom.injective_codRestrict`, `cfcₙ_apply_mkD`, `cfcₙHom_id`, `range_cfcₙHom`, `NonUnitalStarSubalgebra.map_map`, `PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe`, `NonUnitalStarAlgHom.prod_fst_snd`, `NonUnitalStarSubalgebra.val_inclusion`, `cfcₙHom_integral`, `NonUnitalStarAlgHom.comp_apply`, `cfcₙAux_id`, `isometry_cfcₙHom`, `cfcₙHom_predicate`, `Unitization.starLift_range`, `NonUnitalStarAlgHom.prod_apply`, `NonUnitalStarAlgHom.inr_apply`, `Unitization.inrNonUnitalStarAlgHom_apply`, `NonUnitalStarSubalgebra.toNonUnitalSubalgebra_subtype`, `NonUnitalStarSubalgebra.range_val`, `Commute.cfcₙHom`, `Unitization.starMap_inr`, `NonUnitalStarSubalgebra.inclusion_mk`, `NonUnitalStarAlgHom.restrictScalars_injective`, `range_cfcₙ_eq_range_cfcₙHom`, `NonUnitalStarSubalgebraClass.coe_subtype`, `NonUnitalStarAlgHom.restrictScalars_apply`, `ContinuousMapZero.nonUnitalStarAlgHom_precomp_apply`, `NonUnitalStarSubalgebra.iSupLift_inclusion`, `NonUnitalStarAlgHom.coe_toNonUnitalAlgHom`, `NonUnitalStarAlgHom.coe_restrictScalars'`, `NonUnitalStarAlgHom.snd_apply`, `NonUnitalStarAlgHom.coe_zero`, `NonUnitalStarAlgHom.prodEquiv_apply`, `cfcₙHom_isClosedEmbedding`, `cfcₙHom_le_iff`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_apply`, `NonUnitalStarAlgHom.coe_one`, `cfcₙHom_eq_cfcₙ_extend`, `NonUnitalStarAlgHom.fst_apply`, `ContinuousMapZero.toContinuousMapHom_toNNReal`, `NonUnitalStarSubalgebra.iSupLift_of_mem`, `DoubleCentralizer.coeHom_apply`, `cfcₙHom_map_quasispectrum`, `spec_cfcₙAux`, `NonUnitalStarAlgHom.coe_coe`, `Unitization.starLift_apply`, `cfcₙHomSuperset_id`, `nnnorm_cfcₙHom`, `NonUnitalStarSubalgebra.inclusion_right`, `NonUnitalStarSubalgebraClass.subtype_injective`, `isClosedEmbedding_cfcₙHom_of_cfcHom`, `NonUnitalStarAlgHom.realContinuousMapZeroOfNNReal_injective`, `IsSelfAdjoint.commute_cfcₙHom`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `Unitization.starMap_apply`, `NonUnitalContinuousFunctionalCalculus.exists_cfc_of_predicate`, `StarAlgHom.coe_toNonUnitalStarAlgHom`, `ContinuousMapZero.toContinuousMapHom_apply`, `NonUnitalStarSubalgebra.toSubring_subtype`, `cfcₙAux_mem_range_inr`, `Pi.evalNonUnitalStarAlgHom_apply`, `NonUnitalStarAlgHom.one_apply`, `cfcₙHom_continuous`, `cfcₙHomSuperset_continuous`, `cfcₙ_apply_pi`, `NonUnitalStarAlgHom.coe_prod`, `Unitization.inrRangeEquiv_apply_coe`, `NonUnitalStarAlgebra.range_id`, `NonUnitalStarAlgHom.coe_mk'`, `NonUnitalStarSubalgebra.inclusion_injective`, `cfcₙL_apply`, `NonUnitalStarAlgHom.coe_inr`, `Unitization.starLift_range_le`, `NonUnitalStarAlgHom.coe_mk`, `NonUnitalStarAlgHom.coe_inl`, `NonUnitalStarAlgHom.ext_iff`, `Unitization.starLift_symm_apply`, `cfcₙHom_of_cfcHom_map_quasispectrum`, `NonUnitalStarAlgHom.coe_id`, `cfcₙHomSuperset_apply`, `cfcₙ_apply`, `ContinuousMapZero.coe_toContinuousMapHom`, `NonUnitalStarAlgHom.subsingleton`, `NonUnitalStarSubalgebraClass.subtype_apply`, `Unitization.inrRangeEquiv_symm_apply`, `NonUnitalStarSubalgebra.iSupLift_mk`, `cfcₙHom_nonneg_iff`, `CStarMatrix.mapₙₐ_apply`, `PositiveLinearMap.gnsNonUnitalStarAlgHom_apply`, `NonUnitalStarSubalgebra.inclusion_self`, `NonUnitalStarSubalgebra.map_id`, `NonUnitalStarAlgHom.zero_apply`, `NonUnitalStarSubalgebra.inclusion_inclusion`, `NonUnitalStarAlgHom.instNonUnitalAlgHomClass`, `NonUnitalStarAlgHom.range_comp`
`StarAlgEquiv` 📖	CompData	88 math math: `Matrix.l2_opNorm_toEuclideanCLM`, `Unitary.conjStarAlgAut_trans_conjStarAlgAut`, `StarAlgEquiv.ofInjective_symm_apply`, `Matrix.kroneckerTMulStarAlgEquiv_symm_apply`, `StarAlgEquiv.ofLeftInverse'_apply`, `StarAlgEquiv.ofStarAlgHom_symm_apply`, `Matrix.cstar_nnnorm_def`, `Unitary.conjStarAlgAut_symm`, `Unitary.conjStarAlgEquiv_unitaryLinearIsometryEquiv`, `StarAlgEquiv.mul_apply`, `CStarMatrix.mapₗ_reindexₐ`, `StarAlgEquiv.ofStarAlgHom_apply`, `StarAlgEquiv.toStarRingEquiv_symm`, `NonUnitalStarSubalgebra.unitizationStarAlgEquiv_apply_coe`, `LinearIsometryEquiv.conjStarAlgEquiv_apply`, `StarAlgEquiv.restrictScalars_symm_apply`, `LinearMap.toMatrixOrthonormal_reindex`, `StarAlgEquiv.aut_mul`, `StarAlgEquiv.coe_toAlgEquiv`, `gelfandStarTransform_naturality`, `gelfandStarTransform_apply_apply`, `StarAlgEquiv.ofInjective_apply`, `StarAlgEquiv.toAlgEquiv_injective`, `LinearMap.toMatrixOrthonormal_apply_apply`, `StarAlgEquiv.coe_refl`, `StarAlgEquiv.one_apply`, `StarAlgEquiv.toStarRingEquiv_eq_coe`, `gelfandStarTransform_symm_apply`, `Matrix.toEuclideanCLM_toLp`, `StarAlgEquiv.rightInverse_symm`, `StarAlgEquiv.toRingEquiv_symm`, `StarAlgEquiv.aut_inv`, `StarAlgEquiv.leftInverse_symm`, `Unitary.conjStarAlgAut_ext_iff'`, `LinearMap.toMatrixOrthonormal_symm_apply`, `StarAlgEquiv.ofBijective_apply`, `StarAlgEquiv.symm_to_ringEquiv`, `StarAlgEquiv.toRingEquiv_eq_coe`, `Matrix.IsHermitian.cfcAux_apply`, `Matrix.ofLp_toEuclideanCLM`, `StarAlgEquiv.coe_ofBijective`, `Matrix.kroneckerTMulStarAlgEquiv_apply`, `StarAlgEquiv.apply_symm_apply`, `CStarMatrix.reindexₐ_apply`, `StarAlgEquiv.symm_bijective`, `Unitary.conjStarAlgAut_apply`, `Unitary.toAlgEquiv_conjStarAlgAut`, `StarAlgEquiv.coe_pow`, `Matrix.coe_toEuclideanCLM_eq_toEuclideanLin`, `LinearMap.toMatrixOrthonormal_apply`, `Unitary.conjStarAlgAut_symm_apply`, `Unitary.toRingEquiv_conjStarAlgAut`, `StarAlgEquiv.coe_symm_toAlgEquiv`, `StarAlgEquiv.symm_apply_apply`, `Matrix.IsHermitian.spectral_theorem`, `StarAlgEquiv.instStarRingEquivClass`, `LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply`, `StarAlgEquiv.coe_trans`, `StarAlgEquiv.restrictScalars_apply`, `CStarMatrix.ofMatrix_eq_ofMatrixStarAlgEquiv`, `StarAlgEquiv.symm_trans_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `Unitary.conjStarAlgAut_mul_apply`, `StarAlgEquiv.ext_iff`, `StarAlgEquiv.ofAlgEquiv_apply`, `Unitization.inrRangeEquiv_apply_coe`, `StarAlgEquiv.restrictScalars_injective`, `StarAlgEquiv.ofInjective'_apply`, `StarAlgEquiv.to_ringEquiv_symm`, `Matrix.IsHermitian.star_mul_self_mul_eq_diagonal`, `Unitary.conjStarAlgAut_symm_unitaryLinearIsometryEquiv`, `StarAlgEquiv.aut_one`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `Matrix.cstar_norm_def`, `StarAlgEquiv.coe_mk`, `StarAlgEquiv.ofLeftInverse'_symm_apply`, `Matrix.IsHermitian.conjStarAlgAut_star_eigenvectorUnitary`, `cfcHom_eq_of_isStarNormal`, `Unitary.conjStarAlgAut_star_apply`, `Matrix.kroneckerStarAlgEquiv_apply`, `Unitization.inrRangeEquiv_symm_apply`, `StarAlgEquiv.trans_apply`, `StarAlgEquiv.instNonUnitalAlgEquivClass`, `LinearIsometryEquiv.conjStarAlgEquiv_apply_apply`, `continuousFunctionalCalculus_map_id`, `StarAlgEquiv.invFun_eq_symm`, `Unitary.conjStarAlgAut_ext_iff`, `Matrix.kroneckerStarAlgEquiv_symm_apply`
`StarAlgHom` 📖	CompData	94 math math: `Matrix.IsHermitian.isClosedEmbedding_cfcAux`, `IsSelfAdjoint.commute_cfcHom`, `StarSubalgebra.inclusion_apply`, `StarSubalgebra.coe_map`, `Unitization.starAlgHom_ext_iff`, `StarAlgHom.prodEquiv_apply`, `cfcHom_continuous`, `cfcL_apply`, `StarAlgHom.snd_apply`, `cfcHom_nonneg_iff`, `cfc_apply_mkD`, `StarAlgHom.coe_prod`, `Unitization.starLift_symm_apply_apply`, `Unitization.starLift_apply_apply`, `cfcHom_isClosedEmbedding`, `BoundedContinuousFunction.coe_toContinuousMapStarₐ`, `StarAlgHom.comp_apply`, `cfcHom_le_iff`, `cfcHom_id`, `StarSubalgebra.mem_comap`, `StarAlgHom.coe_mk'`, `StarAlgHom.coe_mk`, `StarAlgHom.realContinuousMapOfNNReal_apply`, `gelfandStarTransform_symm_apply`, `StarSubalgebra.subtype_apply`, `Unitization.starMap_injective`, `StarAlgHom.instStarHomClass`, `StarAlgHom.ext_iff`, `StarAlgHom.coe_coe`, `StarSubalgebra.isClosedEmbedding_inclusion`, `cfcHom_integral`, `Unitization.starLift_range`, `ContinuousFunctionalCalculus.exists_cfc_of_predicate`, `StarAlgHom.coe_toAlgHom`, `StarAlgHom.restrictScalars_apply`, `cfc_def`, `Unitization.starMap_inl`, `StarAlgHom.realContinuousMapOfNNReal_apply_comp_toReal`, `Unitization.starMap_inr`, `NonUnitalStarSubalgebra.unitization_injective`, `NonUnitalStarSubalgebra.unitization_apply`, `Unitization.starMap_surjective`, `Matrix.IsHermitian.cfcAux_apply`, `StarSubalgebra.coe_subtype`, `StarAlgHom.ofId_apply`, `continuous_cfcHomSuperset_left`, `PositiveLinearMap.gnsStarAlgHom_apply`, `StarAlgHom.prod_fst_snd`, `cfcHomSuperset_apply`, `StarAlgHom.coe_comp`, `cfcHom_eq_cfc_extend`, `Unitization.starLift_apply`, `SpectrumRestricts.starAlgHom_apply`, `StarAlgHom.instAlgHomClass`, `Commute.cfcHom`, `ContinuousMap.evalStarAlgHom_apply`, `ContinuousMap.nonUnitalStarAlgebraAdjoin_id_subset_ker_evalStarAlgHom`, `cfc_apply`, `QuasispectrumRestricts.nonUnitalStarAlgHom_apply`, `Unitization.starMap_apply`, `StarAlgHom.realContinuousMapOfNNReal_injective`, `cfcHom_isStrictlyPositive_iff`, `StarAlgHom.coe_toNonUnitalStarAlgHom`, `BoundedContinuousFunction.toContinuousMapStarₐ_apply_apply`, `Homeomorph.compStarAlgEquiv'_apply`, `cfc_apply_pi`, `StarSubalgebra.coe_comap`, `Matrix.IsHermitian.cfcAux_id`, `StarAlgHom.prod_apply`, `cfcHomSuperset_id`, `StarAlgHom.prodEquiv_symm_apply`, `StarSubalgebra.inclusion_injective`, `cfcHom_predicate`, `norm_cfcHom`, `ContinuousMap.ker_evalStarAlgHom_inter_adjoin_id`, `cfcHomSuperset_continuous`, `Unitization.starLift_range_le`, `ContinuousMap.compStarAlgHom'_apply`, `Homeomorph.compStarAlgEquiv'_symm_apply`, `nnnorm_cfcHom`, `Pi.evalStarAlgHom_apply`, `ContinuousMap.ker_evalStarAlgHom_eq_closure_adjoin_id`, `Unitization.starLift_symm_apply`, `StarSubalgebra.mem_map`, `StarAlgHom.map_adjoin`, `cfcHom_mono`, `IsometricContinuousFunctionalCalculus.isometric`, `StarAlgHom.coe_id`, `StarAlgHom.restrictScalars_injective`, `cfcHom_map_spectrum`, `StarSubalgebra.isEmbedding_inclusion`, `StarAlgHom.fst_apply`, `cfcHom_apply_mem_elemental`, `isometry_cfcHom`
`«term_→⋆ₐ[_]_»` 📖	CompOp	—
`«term_→⋆ₐ_»` 📖	CompOp	—
`«term_→⋆ₙₐ[_]_»` 📖	CompOp	—
`«term_→⋆ₙₐ_»` 📖	CompOp	—
`«term_≃⋆ₐ[_]_»` 📖	CompOp	—
`«term_≃⋆ₐ_»` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instAlgEquivClassOfNonUnitalAlgEquivClass` 📖	mathematical	—	`AlgEquivClass`	—	`NonUnitalAlgEquivClass.toRingEquivClass` `Algebra.algebraMap_eq_smul_one` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingEquivClass.toRingHomClass`
`instNonUnitalAlgHomClassOfNonUnitalAlgEquivClass` 📖	mathematical	—	`NonUnitalAlgHomClass` `EquivLike.toFunLike`	—	`NonUnitalAlgEquivClass.toMulActionSemiHomClass` `NonUnitalRingHomClass.toAddMonoidHomClass` `RingEquivClass.toNonUnitalRingHomClass` `NonUnitalAlgEquivClass.toRingEquivClass` `NonUnitalRingHomClass.toMulHomClass`

---

← Back to Index