Unital

📁 Source: Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Statistics

Metric	Count
Definitions UniqueHom, cfc, cfcHom, cfcHomSuperset, cfcL, cfcUnits	6
Theorems eq_algebraMap_of_spectrum_subset_singleton, eq_one_of_spectrum_subset_one, eq_zero_of_spectrum_subset_zero, inv_nonneg, inv_nonneg_of_nonneg, le_one, le_one_iff, one_le, one_le_iff, spectrum_algebraMap_eq, spectrum_algebraMap_subset, spectrum_nonempty, spectrum_one_eq, spectrum_zero_eq, compactSpace_spectrum, exists_cfc_of_predicate, isCompact_spectrum, predicate_zero, spectrum_nonempty, eq_of_continuous_of_map_id, cfc, cfc_map, ext_continuousMap, isStrictlyPositive_iff_spectrum_pos, nonneg_iff_spectrum_nonneg, continuousOn_inv₀_spectrum, continuousOn_zpow₀_spectrum, algebraMap_le_cfc, algebraMap_le_cfc_iff, algebraMap_le_iff_le_spectrum, algebraMap_le_of_le_spectrum, cfcHomSuperset_apply, cfcHomSuperset_continuous, cfcHomSuperset_id, cfcHom_comp, cfcHom_continuous, cfcHom_eq_cfc_extend, cfcHom_eq_of_continuous_of_map_id, cfcHom_id, cfcHom_isClosedEmbedding, cfcHom_isStrictlyPositive_iff, cfcHom_le_iff, cfcHom_map_spectrum, cfcHom_mono, cfcHom_nonneg_iff, cfcHom_predicate, cfcL_apply, cfcUnits_pow, cfcUnits_zpow, cfc_add, cfc_add_const, cfc_algebraMap, cfc_apply, cfc_apply_mkD, cfc_apply_of_not_and, cfc_apply_of_not_continuousOn, cfc_apply_of_not_predicate, cfc_apply_one, cfc_apply_pi, cfc_apply_zero, cfc_cases, cfc_commute_cfc, cfc_comp, cfc_comp', cfc_comp_const_mul, cfc_comp_inv, cfc_comp_neg, cfc_comp_polynomial, cfc_comp_pow, cfc_comp_smul, cfc_comp_star, cfc_comp_zpow, cfc_congr, cfc_const, cfc_const_add, cfc_const_mul, cfc_const_mul_id, cfc_const_one, cfc_const_zero, cfc_def, cfc_eq_cfcL, cfc_eq_cfcL_mkD, cfc_eq_cfc_iff_eqOn, cfc_eval_C, cfc_eval_X, cfc_id, cfc_id', cfc_inv, cfc_inv_id, cfc_isStrictlyPositive_iff, cfc_le_algebraMap, cfc_le_algebraMap_iff, cfc_le_iff, cfc_le_one, cfc_le_one_iff, cfc_map_div, cfc_map_polynomial, cfc_map_spectrum, cfc_mono, cfc_mul, cfc_neg, cfc_neg_id, cfc_nonneg, cfc_nonneg_iff, cfc_nonneg_of_predicate, cfc_nonpos, cfc_nonpos_iff, cfc_one, cfc_polynomial, cfc_pow, cfc_pow_id, cfc_predicate, cfc_predicate_algebraMap, cfc_predicate_one, cfc_predicate_zero, cfc_smul, cfc_smul_id, cfc_star, cfc_star_id, cfc_sub, cfc_sum, cfc_sum_univ, cfc_zero, cfc_zpow, eqOn_of_cfc_eq_cfc, isUnit_cfc, isUnit_cfc_iff, le_algebraMap_iff_spectrum_le, le_algebraMap_of_spectrum_le, one_le_cfc, one_le_cfc_iff, range_cfc_eq_range_cfcHom, val_cfcUnits, val_inv_cfcUnits	134
Total	140

CFC

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_algebraMap_of_spectrum_subset_singleton 📖	mathematical	Set Set.instHasSubset spectrum Set.instSingletonSet	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	cfc_id cfc_const cfc_congr
eq_one_of_spectrum_subset_one 📖	mathematical	Set Set.instHasSubset spectrum Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_algebraMap_of_spectrum_subset_singleton
eq_zero_of_spectrum_subset_zero 📖	mathematical	Set Set.instHasSubset spectrum Set.instSingletonSet MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eq_algebraMap_of_spectrum_subset_singleton
inv_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar inv_nonneg_of_nonneg inv_inv
inv_nonneg_of_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	Units Units.instInv	—	NNReal.instIsTopologicalSemiring NNReal.instContinuousStar cfc_predicate cfc_inv_id NNReal.instContinuousInv₀
le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_algebraMap_of_spectrum_le
le_one_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass le_algebraMap_iff_spectrum_le
one_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_le_of_le_spectrum
one_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_le_iff_le_spectrum
spectrum_algebraMap_eq 📖	mathematical	—	spectrum DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap Set Set.instSingletonSet	—	cfc_predicate_zero cfc_const cfc_map_spectrum continuousOn_const Set.Nonempty.image_const spectrum.zero_mem not_isUnit_zero
spectrum_algebraMap_subset 📖	mathematical	—	Set Set.instHasSubset spectrum DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap Set.instSingletonSet	—	cfc_const cfc_predicate_zero cfc_map_spectrum continuousOn_const
spectrum_nonempty 📖	mathematical	—	Set.Nonempty spectrum	—	one_ne_zero NeZero.one cfc_one cfc_zero cfc_congr
spectrum_one_eq 📖	mathematical	—	spectrum AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Set Set.instSingletonSet AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass spectrum_algebraMap_eq
spectrum_zero_eq 📖	mathematical	—	spectrum MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Set Set.instSingletonSet NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass spectrum_algebraMap_eq

ContinuousFunctionalCalculus

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compactSpace_spectrum 📖	mathematical	—	CompactSpace Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	—
exists_cfc_of_predicate 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike ContinuousMap.restrict ContinuousMap.id Set.range ContinuousMap.instFunLike	—	—
isCompact_spectrum 📖	mathematical	—	IsCompact UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	—	isCompact_iff_compactSpace compactSpace_spectrum
predicate_zero 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
spectrum_nonempty 📖	mathematical	—	Set.Nonempty spectrum	—	—

ContinuousMap

Definitions

Name	Category	Theorems
UniqueHom 📖	CompData	4 math math: NNReal.instContinuousMap.UniqueHom, RCLike.instContinuousMapUniqueHom, Real.instContinuousMapUniqueHom, Complex.instContinuousMapUniqueHom

ContinuousMap.UniqueHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_of_continuous_of_map_id 📖	—	Continuous ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike ContinuousMap.restrict ContinuousMap.id	—	—	—

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid cfc	—	cfc_predicate

IsStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc_map 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid cfc	—	Commute.eq_1 SemiconjBy.eq_1 cfc_star cfc_mul ContinuousOn.star mul_comm cfc_apply_of_not_continuousOn star_zero MulZeroClass.mul_zero

StarAlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_continuousMap 📖	—	Continuous ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instFunLike ContinuousMap.restrict ContinuousMap.id	—	—	ContinuousMap.UniqueHom.eq_of_continuous_of_map_id

StarOrderedRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStrictlyPositive_iff_spectrum_pos 📖	mathematical	—	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Preorder.toLT NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	cfc_isStrictlyPositive_iff continuousOn_id' cfc_id
nonneg_iff_spectrum_nonneg 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	cfc_nonneg_iff continuousOn_id' cfc_id

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_inv₀_spectrum 📖	mathematical	—	ContinuousOn InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero spectrum Semifield.toCommSemiring val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	ContinuousOn.mono continuousOn_inv₀ spectrum.zero_notMem isUnit
continuousOn_zpow₀_spectrum 📖	mathematical	—	ContinuousOn DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring spectrum Semifield.toCommSemiring val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	ContinuousOn.mono continuousOn_zpow₀ spectrum.zero_notMem isUnit

(root)

Definitions

Name	Category	Theorems
cfc 📖	CompOp	179 math math: isUnit_cfc_iff, isUnit_cfc, cfc_le_algebraMap_iff, cfc_sum_univ, cfc_pow, CFC.abs_eq_cfc_norm, Filter.Tendsto.cfc, nnnorm_cfc_lt, StarAlgHom.map_cfc, CFC.tendsto_cfc_rpow_sub_one_log, Matrix.IsHermitian.cfc_eq, cfc_const_zero, integrableOn_cfc', Unitization.real_cfcₙ_eq_cfc_inr, norm_cfc_lt_iff, cfc_map_div, cfc_const_one, cfc_commute_cfc, tendsto_cfc_fun, cfc_comp_star, cfc_comp_smul, cfc_apply_one, cfc_apply_of_not_and, ContinuousAt.cfc, cfc_sub, cfc_complex_eq_real, norm_cfc_le_iff, Continuous.cfc', cfc_apply_mkD, cfc_nonneg_iff, Continuous.cfc_nnreal', CFC.rpow_def, ContinuousOn.cfc_nnreal', IsGreatest.nnnorm_cfc_nnreal, ContinuousOn.cfc, cfcₙ_eq_cfc, cfc_map_prod, cfc_comp_pow, cfc_id', Commute.cfc_real, cfc_map_spectrum, Matrix.IsHermitian.charpoly_cfc_eq, lipschitzOnWith_cfc_fun_of_subset, cfc_real_eq_nnreal, continuousOn_cfc_setProd, IsGreatest.norm_cfc, IsSelfAdjoint.cfc, IsGreatest.nnnorm_cfc, cfc_nonpos_iff, cfc_map_polynomial, continuousOn_cfc_nnreal, cfc_nnreal_eq_real, Continuous.cfc_fun, one_le_cfc_iff, CFC.exp_eq_normedSpace_exp, IsSelfAdjoint.cfc_arg, cfc_add_const, val_cfcUnits, cfc_def, cfc_comp', cfc_sum, lipschitzOnWith_cfc_fun, Continuous.cfc_nnreal_of_mem_nhdsSet, cfc_apply_zero, ContinuousOn.cfc_nnreal_of_mem_nhdsSet, cfc_eq_cfc_iff_eqOn, cfc_mono, cfc_le_algebraMap, CFC.rpow_neg_one_eq_cfc_inv, algebraMap_le_cfc, nnnorm_cfc_le_iff, cfc_inv, cfc_neg, cfc_comp_zpow, Continuous.cfc_of_mem_nhdsSet, ContinuousOn.cfc_nnreal, cfc_integral, nnnorm_cfc_nnreal_lt, continuousWithinAt_cfc_fun, cfc_zpow, cfc_eq_cfcL_mkD, nnnorm_cfc_nnreal_le, cfc_nnreal_le_iff, Continuous.cfc_nnreal, ContinuousOn.cfc_of_mem_nhdsSet, nnnorm_cfc_nnreal_le_iff, range_cfc_eq_range_cfcHom, cfc_inv_id, one_le_cfc, cfc_star_id, cfc_one, cfc_nonneg, val_inv_cfcUnits, cfc_const, cfc_eval_C, cfcHom_eq_cfc_extend, range_cfc_nnreal, nnnorm_cfc_le, cfc_comp, Unitization.nnreal_cfcₙ_eq_cfc_inr, integrable_cfc', nnnorm_apply_le_nnnorm_cfc, Continuous.cfc, cfc_apply_mem_elemental, cfc_apply, cfc_polynomial, cfc_comp_norm, apply_le_nnnorm_cfc_nnreal, cfc_nonneg_of_predicate, Commute.cfc, range_cfc_nnreal_eq_image_cfc_real, IsStarNormal.cfc_map, cfc_comp_neg, cfc_smul, cfc_const_add, cfc_apply_of_not_predicate, cfc_zero, norm_cfc_le, cfc_le_iff, cfc_apply_pi, cfc_unitary_iff, ContinuousOn.cfc', cfc_map_pi, cfc_mul, CFC.sqrt_eq_cfc, ContinuousOn.cfc_fun, cfc_id, Filter.Tendsto.cfc_nnreal, nnnorm_cfc_lt_iff, cfc_le_one, Unitization.complex_cfcₙ_eq_cfc_inr, cfc_smul_id, cfc_eq_cfcL, cfc_tsub, norm_apply_le_norm_cfc, integrable_cfc, cfc_predicate, nnnorm_cfc_nnreal_lt_iff, cfc_real_eq_complex, Commute.cfc_nnreal, cfc_comp_const_mul, cfc_congr, MonotoneOn.nnnorm_cfc, cfc_setIntegral', cfc_le_one_iff, continuousOn_cfc_nnreal_setProd, cfc_const_mul_id, integrableOn_cfc, cfc_cases, continuousOn_cfc, cfc_pow_id, cfc_isStrictlyPositive_iff, cfc_algebraMap, cfc_apply_of_not_continuousOn, cfc_star, ContinuousAt.cfc_nnreal, Unitary.argSelfAdjoint_coe, ContinuousWithinAt.cfc, cfc_eval_X, ContinuousWithinAt.cfc_nnreal, CFC.real_exp_eq_normedSpace_exp, range_cfc, SpectrumRestricts.cfc_eq_restrict, CFC.complex_exp_eq_normedSpace_exp, StarAlgHomClass.map_cfc, IsSelfAdjoint.commute_cfc, cfc_setIntegral, cfc_const_mul, cfc_comp_inv, norm_cfc_lt, cfc_neg_id, cfc_add, cfc_integral', CFC.rpow_eq_cfc_real, continuousAt_cfc_fun, cfc_comp_polynomial, cfc_nonpos, Unitization.cfcₙ_eq_cfc_inr, algebraMap_le_cfc_iff
cfcHom 📖	CompOp	31 math math: IsSelfAdjoint.commute_cfcHom, SpectrumRestricts.cfcHom_eq_restrict, cfcHom_eq_of_continuous_of_map_id, cfcHom_continuous, cfcL_apply, cfcHom_nonneg_iff, cfc_apply_mkD, cfcHom_isClosedEmbedding, cfcHom_le_iff, cfcHom_id, cfcHom_integral, cfc_def, cfcHom_real_eq_restrict, cfcHomSuperset_apply, range_cfc_eq_range_cfcHom, cfcHom_nnreal_eq_restrict, cfcHom_eq_cfc_extend, Commute.cfcHom, cfc_apply, cfcHom_isStrictlyPositive_iff, cfc_apply_pi, cfcHom_predicate, norm_cfcHom, range_cfcHom, nnnorm_cfcHom, cfcHom_mono, IsometricContinuousFunctionalCalculus.isometric, cfcHom_eq_of_isStarNormal, cfcHom_map_spectrum, cfcHom_apply_mem_elemental, isometry_cfcHom
cfcHomSuperset 📖	CompOp	4 math math: continuous_cfcHomSuperset_left, cfcHomSuperset_apply, cfcHomSuperset_id, cfcHomSuperset_continuous
cfcL 📖	CompOp	5 math math: cfcL_apply, cfcL_integrable, cfc_eq_cfcL_mkD, cfcL_integral, cfc_eq_cfcL
cfcUnits 📖	CompOp	4 math math: val_cfcUnits, cfcUnits_pow, val_inv_cfcUnits, cfcUnits_zpow

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_le_cfc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap cfc	—	cfc_mono continuousOn_const cfc_const
algebraMap_le_cfc_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Preorder.toLE PartialOrder.toPreorder DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicalRing.toIsTopologicalSemiring cfc_const cfc_le_iff continuousOn_const
algebraMap_le_iff_le_spectrum 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	IsTopologicalRing.toIsTopologicalSemiring cfc_id algebraMap_le_cfc_iff continuousOn_id'
algebraMap_le_of_le_spectrum 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	cfc_id algebraMap_le_cfc continuousOn_id'
cfcHomSuperset_apply 📖	mathematical	Set Set.instHasSubset spectrum	DFunLike.coe StarAlgHom ContinuousMap Set.Elem instTopologicalSpaceSubtype Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHomSuperset cfcHom ContinuousMap.comp Subtype.map	—	—
cfcHomSuperset_continuous 📖	mathematical	Set Set.instHasSubset spectrum	Continuous ContinuousMap Set.Elem instTopologicalSpaceSubtype Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHomSuperset	—	Continuous.comp cfcHom_continuous ContinuousMap.continuous_precomp
cfcHomSuperset_id 📖	mathematical	Set Set.instHasSubset spectrum	DFunLike.coe StarAlgHom ContinuousMap Set.Elem instTopologicalSpaceSubtype Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHomSuperset ContinuousMap.restrict ContinuousMap.id	—	cfcHom_id
cfcHom_comp 📖	mathematical	DFunLike.coe ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instFunLike StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	ContinuousMap.comp cfcHom_predicate	—	cfcHom_predicate cfcHom_eq_of_continuous_of_map_id Continuous.comp Topology.IsClosedEmbedding.continuous cfcHom_isClosedEmbedding ContinuousMap.continuous_precomp ContinuousMap.ext DFunLike.congr_fun
cfcHom_continuous 📖	mathematical	—	Continuous ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	—	Topology.IsClosedEmbedding.continuous cfcHom_isClosedEmbedding
cfcHom_eq_cfc_extend 📖	mathematical	—	DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom cfc Function.extend ContinuousMap.instFunLike	—	Function.Injective.extend_apply continuousOn_iff_continuous_restrict ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass ContinuousOn.restrict cfc_apply ContinuousMap.continuous_toFun
cfcHom_eq_of_continuous_of_map_id 📖	mathematical	Continuous ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike ContinuousMap.restrict ContinuousMap.id	cfcHom	—	StarAlgHom.ext_continuousMap ContinuousFunctionalCalculus.compactSpace_spectrum Topology.IsClosedEmbedding.continuous cfcHom_isClosedEmbedding cfcHom_id
cfcHom_id 📖	mathematical	—	DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom ContinuousMap.restrict ContinuousMap.id	—	ContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcHom_isClosedEmbedding 📖	mathematical	—	Topology.IsClosedEmbedding ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	—	ContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcHom_isStrictlyPositive_iff 📖	mathematical	—	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid StarAlgHom.instFunLike cfcHom Preorder.toLT ContinuousMap.instFunLike	—	IsStrictlyPositive.spectrum_pos Set.mem_range_self cfcHom_map_spectrum cfcHom_nonneg_iff le_of_lt spectrum.isUnit_of_zero_notMem
cfcHom_le_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum CommRing.toCommSemiring instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom ContinuousMap.partialOrder	—	IsTopologicalRing.toIsTopologicalSemiring sub_nonneg covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid IsTopologicalRing.to_topologicalAddGroup map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass cfcHom_nonneg_iff IsTopologicalSemiring.toContinuousAdd ContinuousMap.instStarOrderedRingOfContinuousSqrt
cfcHom_map_spectrum 📖	mathematical	—	spectrum DFunLike.coe StarAlgHom ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom Set.range ContinuousMap.instFunLike	—	ContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcHom_mono 📖	mathematical	ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Preorder.toLE PartialOrder.toPreorder ContinuousMap.partialOrder	DFunLike.coe StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	—	OrderHomClass.mono StarRingHomClass.instOrderHomClass ContinuousMap.instStarOrderedRingOfContinuousSqrt NonUnitalAlgHomClass.toNonUnitalRingHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass NonUnitalStarAlgHomClass.instNonUnitalStarRingHomClassOfStarHomClass StarAlgHom.instStarHomClass
cfcHom_nonneg_iff 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring StarAlgHom.instFunLike cfcHom ContinuousMap.partialOrder ContinuousMap.instZero	—	spectrum_nonneg_of_nonneg cfcHom_map_spectrum map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass cfcHom_mono
cfcHom_predicate 📖	mathematical	—	DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom	—	ContinuousFunctionalCalculus.exists_cfc_of_predicate
cfcL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousMap.module Semiring.toModule SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Algebra.toModule Ring.toSemiring ContinuousLinearMap.funLike cfcL StarAlgHom ContinuousMap.instSemiringOfIsTopologicalSemiring ContinuousMap.algebra ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid StarAlgHom.instFunLike cfcHom	—	IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul
cfcUnits_pow 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Monoid.toNatPow Units.instMonoid cfcUnits DivisionSemiring.toSemiring Semifield.toDivisionSemiring forall₂_imp Set Set.instMembership MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain ContinuousOn.pow IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	—	Units.ext forall₂_imp pow_ne_zero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain ContinuousOn.pow IsTopologicalSemiring.toContinuousMul pow_zero cfcUnits.congr_simp cfc_const_one cfc_pow
cfcUnits_zpow 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring DivInvMonoid.toZPow Units.instDivInvMonoid cfcUnits Pi.instPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring forall₂_imp Set Set.instMembership MulZeroClass.toZero MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring zpow_ne_zero ContinuousOn.zpow₀ IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	—	forall₂_imp zpow_ne_zero ContinuousOn.zpow₀ IsTopologicalSemiring.toContinuousMul zpow_natCast cfcUnits.congr_simp cfcUnits_pow zpow_negSucc Units.ext cfc_pow ContinuousOn.inv₀
cfc_add 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ContinuousOn.restrict cfc_apply IsTopologicalSemiring.toContinuousAdd map_add SemilinearMapClass.toAddHomClass SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass ContinuousOn.fun_add cfc_apply_of_not_predicate add_zero
cfc_add_const 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Ring.toSemiring RingHom.instFunLike algebraMap	—	add_comm cfc.congr_simp cfc_const_add
cfc_algebraMap 📖	mathematical	—	cfc DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	ContinuousOn.mono continuousOn_singleton CFC.spectrum_algebraMap_subset cfc_predicate_algebraMap ContinuousOn.restrict cfc_apply AlgHomClass.commutes StarAlgHom.instAlgHomClass
cfc_apply 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc DFunLike.coe StarAlgHom ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom Set.restrict ContinuousOn.restrict	—	ContinuousOn.restrict cfc_def
cfc_apply_mkD 📖	mathematical	—	cfc DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom ContinuousMap.mkD Set.restrict ContinuousMap.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ContinuousOn.restrict cfc_apply ContinuousMap.mkD_of_continuousOn cfc_apply_of_not_continuousOn ContinuousMap.mkD_of_not_continuousOn map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass
cfc_apply_of_not_and 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_def
cfc_apply_of_not_continuousOn 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_def
cfc_apply_of_not_predicate 📖	mathematical	—	cfc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_def
cfc_apply_one 📖	mathematical	—	cfc AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	cfc.congr_simp map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cfc_algebraMap
cfc_apply_pi 📖	mathematical	—	cfc DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom Set.restrict ContinuousOn.restrict	—	ContinuousOn.restrict cfc_apply
cfc_apply_zero 📖	mathematical	—	cfc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap NonAssocSemiring.toNonUnitalNonAssocSemiring	—	cfc.congr_simp map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cfc_algebraMap
cfc_cases 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe StarAlgHom ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring StarAlgHom.instFunLike cfcHom Set.restrict ContinuousOn.restrict	cfc	—	ContinuousOn.restrict cfc_apply cfc_apply_of_not_predicate cfc_apply_of_not_continuousOn
cfc_commute_cfc 📖	mathematical	—	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing cfc	—	cfc_cases ContinuousOn.restrict Commute.map NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass Commute.all
cfc_comp 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image spectrum	cfc	—	ContinuousOn.comp Set.mapsTo_image ContinuousOn.restrict cfcHom_map_spectrum Set.ext Set.range_restrict cfc_apply cfcHom_predicate Continuous.codRestrict cfcHom_comp
cfc_comp' 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image spectrum	cfc	—	cfc_comp
cfc_comp_const_mul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring spectrum	cfc Algebra.toSMul Ring.toSemiring	—	cfc_comp' ContinuousOn.fun_mul IsTopologicalSemiring.toContinuousMul continuousOn_const continuousOn_id' cfc_const_mul_id
cfc_comp_inv 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	cfc Units Units.instInv	—	cfc_comp' Units.continuousOn_inv₀_spectrum cfc_inv_id
cfc_comp_neg 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing spectrum CommRing.toCommSemiring	cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicalRing.toIsTopologicalSemiring cfc_comp' ContinuousOn.neg IsTopologicalRing.toContinuousNeg continuousOn_id' cfc_neg_id
cfc_comp_polynomial 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image Polynomial.eval CommSemiring.toSemiring spectrum	cfc DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	cfc_comp' Polynomial.continuousOn cfc_polynomial
cfc_comp_pow 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring spectrum	cfc Ring.toSemiring	—	cfc_comp' ContinuousOn.pow IsTopologicalSemiring.toContinuousMul continuousOn_id' cfc_pow_id
cfc_comp_smul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image spectrum	cfc SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_comp' ContinuousOn.const_smul continuousOn_id' cfc_smul_id
cfc_comp_star 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid spectrum	cfc NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_comp' ContinuousOn.star continuousOn_id' cfc_star_id
cfc_comp_zpow 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.image DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring spectrum Semifield.toCommSemiring Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	cfc Units Units.instDivInvMonoid	—	cfc_comp' Units.continuousOn_zpow₀_spectrum IsTopologicalSemiring.toContinuousMul cfc_zpow
cfc_congr 📖	mathematical	Set.EqOn spectrum	cfc	—	ContinuousOn.restrict ContinuousOn.congr cfc_apply Set.restrict_eq_iff not_and_or cfc_apply_of_not_predicate cfc_apply_of_not_continuousOn Set.EqOn.symm
cfc_const 📖	mathematical	—	cfc DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	ContinuousOn.restrict continuousOn_const cfc_apply AlgHomClass.commutes StarAlgHom.instAlgHomClass
cfc_const_add 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe RingHom Ring.toSemiring RingHom.instFunLike algebraMap	—	cfc_add continuousOn_const cfc_const
cfc_const_mul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toSMul Ring.toSemiring	—	cfc_smul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower IsScalarTower.right
cfc_const_mul_id 📖	mathematical	—	cfc Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Algebra.toSMul Ring.toSemiring	—	cfc_smul_id SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower IsScalarTower.right
cfc_const_one 📖	mathematical	—	cfc AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	cfc_one
cfc_const_zero 📖	mathematical	—	cfc MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_zero
cfc_def 📖	mathematical	—	cfc ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum DFunLike.coe StarAlgHom ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring StarRing.toStarAddMonoid Ring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarAlgHom.instFunLike cfcHom Set.restrict MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	—
cfc_eq_cfcL 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousMap Set.Elem instTopologicalSpaceSubtype Set Set.instMembership ContinuousMap.compactOpen ContinuousMap.instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousMap.module Semiring.toModule SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Algebra.toModule Ring.toSemiring ContinuousLinearMap.funLike cfcL Set.restrict ContinuousOn.restrict	—	IsTopologicalSemiring.toContinuousAdd SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul ContinuousOn.restrict cfc_def cfcL_apply
cfc_eq_cfcL_mkD 📖	mathematical	—	cfc DFunLike.coe ContinuousLinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.compactOpen ContinuousMap.instAddCommMonoidOfContinuousAdd NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring IsTopologicalSemiring.toContinuousAdd NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousMap.module Semiring.toModule SMulCommClass.continuousConstSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id IsTopologicalSemiring.toContinuousMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Algebra.toModule Ring.toSemiring ContinuousLinearMap.funLike cfcL ContinuousMap.mkD Set.restrict ContinuousMap.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	cfc_apply_mkD
cfc_eq_cfc_iff_eqOn 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Set.EqOn	—	eqOn_of_cfc_eq_cfc cfc_congr
cfc_eval_C 📖	mathematical	—	cfc Polynomial.eval CommSemiring.toSemiring DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Ring.toSemiring algebraMap	—	cfc.congr_simp Polynomial.eval_C cfc_const
cfc_eval_X 📖	mathematical	—	cfc Polynomial.eval CommSemiring.toSemiring Polynomial.X	—	cfc.congr_simp Polynomial.eval_X cfc_id
cfc_id 📖	mathematical	—	cfc	—	ContinuousOn.restrict continuousOn_id' cfcHom_id cfc_apply
cfc_id' 📖	mathematical	—	cfc	—	cfc_id
cfc_inv 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	cfc InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Ring.inverse Semiring.toMonoidWithZero Ring.toSemiring	—	val_inv_cfcUnits val_cfcUnits Ring.inverse_unit
cfc_inv_id 📖	mathematical	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	cfc Semifield.toCommSemiring InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Units Units.instInv	—	Ring.inverse_unit cfc_id cfc_inv spectrum.zero_notMem Units.isUnit continuousOn_id'
cfc_isStrictlyPositive_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	IsStrictlyPositive Preorder.toLE PartialOrder.toPreorder MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing cfc Preorder.toLT NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	ContinuousOn.restrict cfc_apply cfcHom_isStrictlyPositive_iff
cfc_le_algebraMap 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	cfc_mono continuousOn_const cfc_const
cfc_le_algebraMap_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Preorder.toLE PartialOrder.toPreorder cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	IsTopologicalRing.toIsTopologicalSemiring cfc_const cfc_le_iff continuousOn_const
cfc_le_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Preorder.toLE PartialOrder.toPreorder cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	IsTopologicalRing.toIsTopologicalSemiring ContinuousOn.restrict cfc_apply cfcHom_le_iff ContinuousMap.le_def
cfc_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfc AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	cfc_cases instZeroLEOneClass ContinuousOn.restrict map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass cfcHom_mono
cfc_le_one_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Preorder.toLE PartialOrder.toPreorder cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass cfc_le_algebraMap_iff
cfc_map_div 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	cfc DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Ring.inverse Semiring.toMonoidWithZero Ring.toSemiring	—	cfc.congr_simp div_eq_mul_inv cfc_mul ContinuousOn.inv₀ cfc_inv
cfc_map_polynomial 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Polynomial.eval CommSemiring.toSemiring DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	Polynomial.induction_on cfc.congr_simp Polynomial.eval_C cfc_const Polynomial.aeval_C Polynomial.eval_add cfc_add Continuous.comp_continuousOn' Polynomial.continuous map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.eval_mul Polynomial.eval_X_pow map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X cfc_const_mul ContinuousOn.pow IsTopologicalSemiring.toContinuousMul cfc_pow smul_eq_mul algebraMap_smul IsScalarTower.right
cfc_map_spectrum 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Set.image	—	ContinuousOn.restrict cfc_apply cfcHom_map_spectrum Set.range_restrict
cfc_mono 📖	mathematical	Preorder.toLE PartialOrder.toPreorder ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc	—	ContinuousOn.restrict cfc_apply cfcHom_mono cfc_apply_of_not_predicate
cfc_mul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ContinuousOn.restrict cfc_apply IsTopologicalSemiring.toContinuousMul map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass ContinuousOn.fun_mul cfc_apply_of_not_predicate MulZeroClass.mul_zero
cfc_neg 📖	mathematical	—	cfc CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring ContinuousOn.restrict cfc_apply IsTopologicalRing.to_topologicalAddGroup map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass ContinuousOn.neg IsTopologicalRing.toContinuousNeg not_and_or cfc_apply_of_not_predicate neg_zero cfc_apply_of_not_continuousOn neg_neg
cfc_neg_id 📖	mathematical	—	cfc CommRing.toCommSemiring IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring cfc_neg cfc_id'
cfc_nonneg 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing cfc	—	cfc_const_zero cfc_mono continuousOn_const cfc_apply_of_not_continuousOn
cfc_nonneg_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing cfc NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	ContinuousOn.restrict cfc_apply cfcHom_nonneg_iff ContinuousMap.le_def
cfc_nonneg_of_predicate 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing cfc	—	cfc_predicate
cfc_nonpos 📖	mathematical	Preorder.toLE PartialOrder.toPreorder MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	cfc NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_const_zero cfc_mono continuousOn_const cfc_apply_of_not_continuousOn
cfc_nonpos_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Preorder.toLE PartialOrder.toPreorder cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	IsTopologicalRing.toIsTopologicalSemiring IsOrderedAddMonoid.toAddLeftMono IsOrderedCancelAddMonoid.toIsOrderedAddMonoid IsOrderedAddMonoid.toIsOrderedCancelAddMonoid StarOrderedRing.toIsOrderedAddMonoid cfc_nonneg_iff ContinuousOn.neg IsTopologicalRing.toContinuousNeg
cfc_one 📖	mathematical	—	cfc Pi.instOne AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	ContinuousOn.restrict Continuous.continuousOn continuous_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass cfc_apply
cfc_polynomial 📖	mathematical	—	cfc Polynomial.eval CommSemiring.toSemiring DFunLike.coe AlgHom Polynomial Polynomial.semiring Ring.toSemiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval	—	cfc_map_polynomial continuousOn_id' cfc_id'
cfc_pow 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Ring.toSemiring	—	ContinuousOn.restrict cfc_apply IsTopologicalSemiring.toContinuousMul map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass ContinuousOn.pow
cfc_pow_id 📖	mathematical	—	cfc Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Ring.toSemiring	—	cfc_pow continuousOn_id' cfc_id'
cfc_predicate 📖	mathematical	—	cfc	—	cfc_cases cfc_predicate_zero cfcHom_predicate ContinuousOn.restrict
cfc_predicate_algebraMap 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	cfc_predicate cfc_const cfc_predicate_zero
cfc_predicate_one 📖	mathematical	—	AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	cfc_predicate_algebraMap map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
cfc_predicate_zero 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ContinuousFunctionalCalculus.predicate_zero
cfc_smul 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	cfc SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ContinuousOn.restrict cfc_apply ContinuousOn.const_smul smul_one_smul SMulCommClass.continuousConstSMul Algebra.to_smulCommClass IsTopologicalSemiring.toContinuousMul map_smul SemilinearMapClass.toMulActionSemiHomClass IsTopologicalSemiring.toContinuousAdd NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass cfc_apply_of_not_predicate smul_zero
cfc_smul_id 📖	mathematical	—	cfc SMulZeroClass.toSMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_smul continuousOn_id' cfc_id'
cfc_star 📖	mathematical	—	cfc Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ContinuousOn.restrict cfc_apply StarHomClass.map_star StarAlgHom.instStarHomClass ContinuousOn.star not_and_or cfc_apply_of_not_predicate star_zero cfc_apply_of_not_continuousOn star_star
cfc_star_id 📖	mathematical	—	cfc Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_star cfc_id'
cfc_sub 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring ContinuousOn.restrict cfc_apply IsTopologicalRing.to_topologicalAddGroup map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub cfc_apply_of_not_predicate sub_self
cfc_sum 📖	mathematical	—	cfc Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	Finset.sum_apply Finset.sum_coe_sort continuousOn_finset_sum IsTopologicalSemiring.toContinuousAdd ContinuousOn.restrict cfc_apply_pi map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass StarAlgHom.instAlgHomClass cfc_apply ContinuousMap.ext ContinuousMap.coe_sum Finset.sum_congr cfc_apply_of_not_predicate Finset.sum_const_zero
cfc_sum_univ 📖	mathematical	—	cfc Finset.sum Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Finset.univ NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	cfc_sum
cfc_zero 📖	mathematical	—	cfc Pi.instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	ContinuousOn.restrict Continuous.continuousOn continuous_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass StarAlgHom.instAlgHomClass cfc_apply cfc_apply_of_not_predicate
cfc_zpow 📖	mathematical	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	cfc Semifield.toCommSemiring DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero Semifield.toDivisionSemiring Units Units.instDivInvMonoid	—	cfc.congr_simp zpow_natCast cfc_pow_id zpow_negSucc cfc_pow Units.continuousOn_inv₀_spectrum cfc_inv_id
eqOn_of_cfc_eq_cfc 📖	mathematical	cfc ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	Set.EqOn	—	ContinuousOn.restrict Topology.IsEmbedding.injective Topology.IsClosedEmbedding.toIsEmbedding cfcHom_isClosedEmbedding cfc_apply
isUnit_cfc 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring cfc	—	isUnit_cfc_iff
isUnit_cfc_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring cfc	—	spectrum.zero_notMem_iff cfc_map_spectrum
le_algebraMap_iff_spectrum_le 📖	mathematical	—	Preorder.toLE PartialOrder.toPreorder DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	IsTopologicalRing.toIsTopologicalSemiring cfc_id cfc_le_algebraMap_iff continuousOn_id'
le_algebraMap_of_spectrum_le 📖	mathematical	Preorder.toLE PartialOrder.toPreorder	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	cfc_id cfc_le_algebraMap continuousOn_id'
one_le_cfc 📖	mathematical	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum	AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne cfc	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_le_cfc
one_le_cfc_iff 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum CommRing.toCommSemiring	Preorder.toLE PartialOrder.toPreorder AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne cfc IsTopologicalRing.toIsTopologicalSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRing.toRing	—	IsTopologicalRing.toIsTopologicalSemiring map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_le_cfc_iff
range_cfc_eq_range_cfcHom 📖	mathematical	—	Set.range cfc SetLike.coe StarSubalgebra Ring.toSemiring StarSubalgebra.setLike StarAlgHom.range ContinuousMap Set.Elem spectrum instTopologicalSpaceSubtype Set Set.instMembership UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace ContinuousMap.instSemiringOfIsTopologicalSemiring CommSemiring.toSemiring ContinuousMap.algebra Algebra.id ContinuousMap.instStarRingOfContinuousStar NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring cfcHom	—	Set.ext cfc_cases ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass SubsemiringClass.toAddSubmonoidClass StarSubalgebra.subsemiringClass ContinuousOn.restrict cfcHom_eq_cfc_extend
val_cfcUnits 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring cfcUnits cfc	—	—
val_inv_cfcUnits 📖	mathematical	ContinuousOn UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace spectrum Semifield.toCommSemiring	Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Units Units.instInv cfcUnits cfc InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero	—	—

---

← Back to Index