Connected

📁 Source: Mathlib/Analysis/CStarAlgebra/Unitary/Connected.lean

Statistics

Metric	Count
Definitions argSelfAdjoint, openPartialHomeomorph, path, expUnitaryPathToOne, argSelfAdjoint, openPartialHomeomorph, path	7
Theorems cfc_arg, argSelfAdjoint_coe, continuousOn_argSelfAdjoint, expUnitary_eq_mul_inv, instLocPathConnectedSpace, isPathConnected_ball, joined, mem_pathComponentOne_iff, norm_argSelfAdjoint, norm_argSelfAdjoint_le_pi, norm_expUnitary_smul_argSelfAdjoint_sub_one_le, norm_sub_eq, norm_sub_one_lt_two_iff, norm_sub_one_sq_eq, openPartialHomeomorph_apply, openPartialHomeomorph_source, openPartialHomeomorph_symm_apply, openPartialHomeomorph_target, path_apply, spectrum_subset_slitPlane_iff_norm_lt_two, two_mul_one_sub_cos_norm_argSelfAdjoint, two_mul_one_sub_le_norm_sub_one_sq, argSelfAdjoint_expUnitary, expUnitary_argSelfAdjoint, expUnitaryPathToOne_apply, joined_one_expUnitary, norm_sq_expUnitary_sub_one, continuousOn_argSelfAdjoint, expUnitary_eq_mul_inv, isPathConnected_ball, joined, mem_pathComponentOne_iff, norm_argSelfAdjoint, norm_argSelfAdjoint_le_pi, norm_expUnitary_smul_argSelfAdjoint_sub_one_le, norm_sub_eq, norm_sub_one_lt_two_iff, norm_sub_one_sq_eq, spectrum_subset_slitPlane_iff_norm_lt_two, two_mul_one_sub_cos_norm_argSelfAdjoint, two_mul_one_sub_le_norm_sub_one_sq	41
Total	48

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cfc_arg 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing StarRing.toStarAddMonoid CStarAlgebra.toStarRing cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField IsTopologicalRing.toIsTopologicalSemiring UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NonUnitalCommCStarAlgebra.toNonUnitalNormedCommRing CommCStarAlgebra.toNonUnitalCommCStarAlgebra instCommCStarAlgebraComplex IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra CStarAlgebra.toNormedAlgebra IsStarNormal.instContinuousFunctionalCalculus Real Complex.ofReal Complex.arg	—	IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus cfc.congr_simp Complex.conj_ofReal

Unitary

Definitions

Name	Category	Theorems
argSelfAdjoint 📖	CompOp	17 math math: unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, norm_expUnitary_smul_argSelfAdjoint_sub_one_le, continuousOn_argSelfAdjoint, expUnitary_eq_mul_inv, unitary.norm_argSelfAdjoint, expUnitary_argSelfAdjoint, argSelfAdjoint_expUnitary, unitary.expUnitary_eq_mul_inv, norm_argSelfAdjoint, unitary.norm_argSelfAdjoint_le_pi, norm_argSelfAdjoint_le_pi, openPartialHomeomorph_apply, argSelfAdjoint_coe, path_apply, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, unitary.continuousOn_argSelfAdjoint, two_mul_one_sub_cos_norm_argSelfAdjoint
openPartialHomeomorph 📖	CompOp	4 math math: openPartialHomeomorph_source, openPartialHomeomorph_symm_apply, openPartialHomeomorph_target, openPartialHomeomorph_apply
path 📖	CompOp	1 math math: path_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
argSelfAdjoint_coe 📖	mathematical	—	AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing argSelfAdjoint cfc Complex IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Complex.instCommSemiring Complex.instStarRing NormedField.toMetricSpace Complex.instNormedField Complex.instContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing NormedAlgebra.toAlgebra CStarAlgebra.toNormedAlgebra IsStarNormal.instContinuousFunctionalCalculus Complex.ofReal Complex.arg Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	—	—
continuousOn_argSelfAdjoint 📖	mathematical	—	ContinuousOn Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing argSelfAdjoint Metric.ball Subtype.pseudoMetricSpace Submonoid.one Real instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Topology.IsInducing.continuousOn_iff Topology.IsInducing.subtypeVal Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus IsOpen.continuousOn_iff Metric.isOpen_ball exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sq_lt_sq₀ IsOrderedRing.toMulPosMono Real.instIsOrderedRing dist_nonneg le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo lt_of_le_of_lt Even.pow_nonneg IsStrictOrderedRing.toIsOrderedRing AddGroup.existsAddOfLE even_two_mul Real.lt_sqrt_of_sq_lt ContinuousOn.continuousAt ContinuousOn.image_comp_continuous ContinuousOn.mono IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsStarNormal.instIsometricContinuousFunctionalCalculus continuousOn_cfc NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing IsCompact.inter_right isCompact_sphere Complex.instProperSpace isClosed_le HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid Continuous.comp' Continuous.fun_mul IsTopologicalSemiring.toContinuousMul instIsTopologicalRingReal continuous_const continuous_id' Continuous.sub IsTopologicalAddGroup.to_continuousSub instIsTopologicalAddGroupReal Complex.continuous_re Continuous.comp_continuousOn Complex.continuous_ofReal Complex.continuousOn_arg Complex.subset_slitPlane_iff_of_subset_sphere Set.inter_subset_left Mathlib.Meta.NormNum.IsInt.neg_to_eq Mathlib.Meta.NormNum.isInt_sub Mathlib.Meta.NormNum.isInt_neg Mathlib.Meta.NormNum.IsNat.to_isInt Nat.cast_one Nat.cast_zero norm_neg CStarRing.norm_of_mem_unitary Complex.instNontrivial Mathlib.Meta.NormNum.IsNat.to_eq SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass sub_neg_eq_add Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 coe_isStarNormal spectrum_subset_circle CStarAlgebra.toCompleteSpace two_mul_one_sub_le_norm_sub_one_sq Real.le_sqrt norm_nonneg dist_eq_norm continuous_subtype_val Metric.closedBall_mem_nhds_of_mem
expUnitary_eq_mul_inv 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule argSelfAdjoint Submonoid.mul Star.star instStarSubtypeMemSubmonoidUnitary	—	Nat.instAtLeastTwoHAddOfNat expUnitary_argSelfAdjoint norm_sub_eq
instLocPathConnectedSpace 📖	mathematical	—	LocPathConnectedSpace Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	LocPathConnectedSpace.of_bases Nat.instAtLeastTwoHAddOfNat nhds_basis_uniformity Metric.uniformity_basis_dist_lt zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid isPathConnected_ball
isPathConnected_ball 📖	mathematical	Real Real.instLT Real.instZero instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	IsPathConnected Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Metric.ball Subtype.pseudoMetricSpace	—	Nat.instAtLeastTwoHAddOfNat dist_self dist_eq_norm LT.lt.trans Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule instTrivialStarReal selfAdjoint.expUnitary.congr_simp star_one mul_one LE.le.trans_lt NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing StarModule.complexToReal norm_expUnitary_smul_argSelfAdjoint_sub_one_le Set.ext inv_mul_cancel Set.image_mul_left CStarRing.norm_coe_unitary_mul IsPathConnected.image Continuous.fun_mul Submonoid.continuousMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing continuous_const continuous_id'
joined 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Joined instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	Nat.instAtLeastTwoHAddOfNat
mem_pathComponentOne_iff 📖	mathematical	—	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing Set Set.instMembership pathComponent instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Submonoid.one Submonoid.mul AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule	—	NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule pathComponent_eq_connectedComponent instLocPathConnectedSpace IsClopen.connectedComponent_subset IsClopen.of_thickening_subset_self Nat.instAtLeastTwoHAddOfNat zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Metric.mem_thickening_iff expUnitary_eq_mul_inv dist_eq_norm SubmonoidClass.toMulMemClass Submonoid.instSubmonoidClass mul_assoc star_mul_self mul_one Joined.mul Submonoid.continuousMul IsTopologicalSemiring.toContinuousMul IsTopologicalRing.toIsTopologicalSemiring NonUnitalSeminormedRing.toIsTopologicalRing selfAdjoint.joined_one_expUnitary
norm_argSelfAdjoint 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	AddSubgroup AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup argSelfAdjoint Real.arccos Real.instSub Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat Real.arccos_eq_of_eq_cos norm_nonneg norm_argSelfAdjoint_le_pi Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.lt_of_lt_of_eq CancelDenoms.sub_subst CancelDenoms.div_subst CancelDenoms.pow_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.one_natPow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Tactic.Linarith.mul_neg Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing Mathlib.Meta.NormNum.isNat_lt_true neg_eq_zero sub_eq_zero_of_eq two_mul_one_sub_cos_norm_argSelfAdjoint
norm_argSelfAdjoint_le_pi 📖	mathematical	—	Real Real.instLE Norm.norm AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup argSelfAdjoint Real.pi	—	norm_cfc_le IsStarNormal.instIsometricContinuousFunctionalCalculus le_of_lt Real.pi_pos Complex.norm_real Complex.abs_arg_le_pi
norm_expUnitary_smul_argSelfAdjoint_sub_one_le 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instLE selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule AddSubgroup AddSubgroup.instSetLike selfAdjoint selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instStarRingReal instTrivialStarReal Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField SeminormedRing.toRing NormedRing.toSeminormedRing NormedAlgebra.toAlgebra NormedAlgebra.complexToReal StarModule.complexToReal NormedAddCommGroup.toAddCommGroup SubNegMonoid.toAddMonoid Algebra.toModule Complex Complex.instNormedField argSelfAdjoint	—	Nat.instAtLeastTwoHAddOfNat instTrivialStarReal StarModule.complexToReal CStarAlgebra.toStarModule one_mul norm_smul NormedSpace.toNormSMulClass abs_of_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid mul_le_mul_of_nonneg_right IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace sq_le_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing selfAdjoint.norm_sq_expUnitary_sub_one LE.le.trans norm_argSelfAdjoint_le_pi mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono sub_le_sub_left covariant_swap_add_of_covariant_add Real.cos_le_cos_of_nonneg_of_le_pi le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Eq.le two_mul_one_sub_cos_norm_argSelfAdjoint
norm_sub_eq 📖	mathematical	—	Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing Submonoid.mul Star.star instStarSubtypeMemSubmonoidUnitary AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	sub_mul mul_assoc star_mul_self_of_mem mul_one one_mul CStarRing.norm_mul_coe_unitary CStarAlgebra.toCStarRing
norm_sub_one_lt_two_iff 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing	Real Real.instLT Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex Set Set.instMembership spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra Complex.instNeg Complex.instOne	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Nat.instAtLeastTwoHAddOfNat norm_of_subsingleton Real.instIsOrderedRing Real.instNontrivial spectrum.of_subsingleton sq_lt_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono norm_nonneg le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo LE.le.trans_lt two_mul_one_sub_le_norm_sub_one_sq sub_neg_eq_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Tactic.Contrapose.contrapose₂ IsCompact.exists_isLeast instClosedIicTopology HasSolidNorm.orderClosedTopology instHasSolidNormReal Real.instIsOrderedAddMonoid IsCompact.image spectrum.isCompact CStarAlgebra.toCompleteSpace Complex.instProperSpace Complex.continuous_re Set.Nonempty.image spectrum.nonempty norm_sub_one_sq_eq le_of_not_gt Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Tactic.Linarith.add_lt_of_le_of_neg Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Tactic.Linarith.mul_neg Mathlib.Tactic.Linarith.sub_neg_of_lt Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike spectrum.norm_eq_one_of_unitary CStarAlgebra.toCStarRing RCLike.re_le_neg_norm_iff_eq_neg_norm RCLike.re_eq_complex_re
norm_sub_one_sq_eq 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing IsLeast Real Real.instLE Set.image Complex Complex.re spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra	Monoid.toNatPow Real.instMonoid Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne	—	Nat.instAtLeastTwoHAddOfNat subsingleton_or_nontrivial Set.Nonempty.ne_empty Set.Nonempty.of_image IsLeast.nonempty spectrum.of_subsingleton IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus cfc_id' isStarNormal_of_mem_unitary cfc_one cfc_sub continuousOn_id' Continuous.continuousOn continuous_one Set.EqOn.mono spectrum.subset_circle_of_unitary CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace Complex.norm_sub_one_sq_eqOn_sphere mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing sub_le_sub_left IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Set.image_image Antitone.map_isLeast MonotoneOn.mono pow_left_monotoneOn IsOrderedRing.toMulPosMono RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsStarNormal.instIsometricContinuousFunctionalCalculus MonotoneOn.map_isGreatest IsGreatest.norm_cfc ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn_const IsGreatest.unique Set.EqOn.image_eq
openPartialHomeomorph_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing openPartialHomeomorph argSelfAdjoint	—	—
openPartialHomeomorph_source 📖	mathematical	—	PartialEquiv.source Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing openPartialHomeomorph Metric.ball Subtype.pseudoMetricSpace Submonoid.one Real instOfNatAtLeastTwo Real.instNatCast	—	—
openPartialHomeomorph_symm_apply 📖	mathematical	—	OpenPartialHomeomorph.toFun' AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing OpenPartialHomeomorph.symm openPartialHomeomorph selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule	—	—
openPartialHomeomorph_target 📖	mathematical	—	PartialEquiv.target Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing OpenPartialHomeomorph.toPartialEquiv instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing openPartialHomeomorph Metric.ball Subtype.pseudoMetricSpace AddSubgroup.zero Real.pi	—	—
path_apply 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	DFunLike.coe Path instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Set.Elem unitInterval Path.instFunLike path Submonoid.mul selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule AddSubgroup AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instStarRingReal instTrivialStarReal Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField SeminormedRing.toRing NormedAlgebra.toAlgebra NormedAlgebra.complexToReal Set Set.instMembership argSelfAdjoint Star.star instStarSubtypeMemSubmonoidUnitary	—	Nat.instAtLeastTwoHAddOfNat
spectrum_subset_slitPlane_iff_norm_lt_two 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing	Set Complex Set.instHasSubset spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra Complex.slitPlane Real Real.instLT Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Nat.instAtLeastTwoHAddOfNat Complex.subset_slitPlane_iff_of_subset_sphere spectrum.subset_circle_of_unitary CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace norm_sub_one_lt_two_iff
two_mul_one_sub_cos_norm_argSelfAdjoint 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instMul Real.instSub Real.instOne Real.cos AddSubgroup AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup argSelfAdjoint Monoid.toNatPow Real.instMonoid	—	Nat.instAtLeastTwoHAddOfNat NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule expUnitary_argSelfAdjoint selfAdjoint.norm_sq_expUnitary_sub_one norm_argSelfAdjoint_le_pi
two_mul_one_sub_le_norm_sub_one_sq 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing Complex Set Set.instMembership spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra	Real Real.instLE Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne Complex.re Monoid.toNatPow Real.instMonoid Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Nat.instAtLeastTwoHAddOfNat Real.sqrt_le_left norm_nonneg spectrum.subset_circle_of_unitary CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus cfc_id' isStarNormal_of_mem_unitary cfc_one cfc_sub continuousOn_id' Continuous.continuousOn continuous_one RCLike.instContinuousStar IsometricContinuousFunctionalCalculus.toContinuousFunctionalCalculus IsStarNormal.instIsometricContinuousFunctionalCalculus Real.sqrt_mul Real.instIsOrderedRing Real.sqrt_sq Complex.norm_sub_one_sq_eq_of_norm_eq_one sub_zero norm_apply_le_norm_cfc ContinuousOn.sub IsTopologicalAddGroup.to_continuousSub SeminormedAddCommGroup.toIsTopologicalAddGroup continuousOn_const

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
argSelfAdjoint_expUnitary 📖	mathematical	Real Real.instLT Norm.norm AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup Real.pi	Unitary.argSelfAdjoint selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule instSubsingletonSubtype_mathlib Nat.instAtLeastTwoHAddOfNat Unitary.spectrum_subset_slitPlane_iff_norm_lt_two sq_lt_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo selfAdjoint.norm_sq_expUnitary_sub_one LT.lt.le mul_lt_mul_of_pos_left sub_lt_sub_left IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add Real.cos_lt_cos_of_nonneg_of_le_pi le_rfl Real.cos_pi sub_neg_eq_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Nat.cast_one Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar CFC.exp_eq_normedSpace_exp IsStarNormal.smul Algebra.to_smulCommClass IsScalarTower.right selfAdjoint.isStarNormal cfc_comp_smul Complex.instContinuousMapUniqueHom TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower Continuous.continuousOn NormedSpace.exp_continuous Complex.instCharZero Complex.instCompleteSpace cfc_comp' Continuous.comp_continuousOn Complex.continuous_ofReal ContinuousOn.mono Complex.continuousOn_arg cfc_map_spectrum Continuous.comp_continuousOn' ContinuousOn.const_smul continuousOn_id' selfAdjoint.expUnitary_coe cfc_id' cfc_congr SpectrumRestricts.algebraMap_image IsScalarTower.complexToReal IsSelfAdjoint.spectrumRestricts NormedSpace.exp.congr_simp mul_comm LE.le.trans_lt spectrum.norm_le_norm_of_mem CStarRing.instNormOneClassOfNontrivial Circle.coe_exp Circle.arg_exp
expUnitary_argSelfAdjoint 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule Unitary.argSelfAdjoint	—	Nat.instAtLeastTwoHAddOfNat NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule ContinuousOn.mono Complex.continuousOn_arg Unitary.spectrum_subset_slitPlane_iff_norm_lt_two selfAdjoint.expUnitary_coe Complex.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus Unitary.argSelfAdjoint_coe IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar CFC.exp_eq_normedSpace_exp IsStarNormal.smul Algebra.to_smulCommClass IsScalarTower.right IsStarNormal.cfc_map cfc_comp_smul Complex.instContinuousMapUniqueHom TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower Continuous.continuousOn NormedSpace.exp_continuous Complex.instCharZero Complex.instCompleteSpace cfc_comp' Continuous.comp_continuousOn' ContinuousOn.const_smul continuousOn_id' Complex.continuous_ofReal Unitary.coe_isStarNormal cfc_id' cfc_congr spectrum.norm_eq_one_of_unitary Complex.ext MulZeroClass.zero_mul MulZeroClass.mul_zero sub_self Complex.log_re Real.log_one one_mul zero_add Complex.log_im NormedSpace.exp.congr_simp Complex.exp_log norm_zero NeZero.charZero_one RCLike.charZero_rclike

selfAdjoint

Definitions

Name	Category	Theorems
expUnitaryPathToOne 📖	CompOp	1 math math: expUnitaryPathToOne_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
expUnitaryPathToOne_apply 📖	mathematical	—	DFunLike.coe Path Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Submonoid.one expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule Set.Elem Real unitInterval Path.instFunLike expUnitaryPathToOne AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup AddSubgroup.instSetLike selfAdjoint instSMulSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instStarRingReal instTrivialStarReal Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField SeminormedRing.toRing NormedAlgebra.toAlgebra NormedAlgebra.complexToReal Set Set.instMembership	—	NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule
joined_one_expUnitary 📖	mathematical	—	Joined Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Submonoid.one expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule	—	NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule
norm_sq_expUnitary_sub_one 📖	mathematical	Real Real.instLE Norm.norm AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup Real.pi	Monoid.toNatPow Real.instMonoid NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne Real.cos	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim NormedStarGroup.to_continuousStar CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule Nat.instAtLeastTwoHAddOfNat norm_of_subsingleton zero_pow Nat.instCharZero Real.cos_zero sub_self MulZeroClass.mul_zero Unitary.norm_sub_one_sq_eq IsTopologicalRing.toIsTopologicalSemiring IsTopologicalDivisionRing.toIsTopologicalRing NormedDivisionRing.to_isTopologicalDivisionRing RCLike.instContinuousStar IsStarNormal.instContinuousFunctionalCalculus CFC.exp_eq_normedSpace_exp IsStarNormal.smul Algebra.to_smulCommClass IsScalarTower.right isStarNormal cfc_comp_smul Complex.instContinuousMapUniqueHom TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace UniformContinuousConstSMul.to_continuousConstSMul Ring.uniformContinuousConstSMul SeminormedAddCommGroup.to_isUniformAddGroup IsTopologicalSemiring.toContinuousMul IsScalarTower.left Pi.isScalarTower Continuous.continuousOn NormedSpace.exp_continuous Complex.instCharZero Complex.instCompleteSpace cfc_map_spectrum Continuous.comp_continuousOn' ContinuousOn.const_smul continuousOn_id' SpectrumRestricts.algebraMap_image IsScalarTower.complexToReal IsSelfAdjoint.spectrumRestricts Set.image_congr NormedSpace.exp.congr_simp mul_comm Set.image_image Complex.exp_ofReal_mul_I_re CStarAlgebra.norm_or_neg_norm_mem_spectrum Real.cos_neg Real.cos_le_cos_of_nonneg_of_le_pi abs_nonneg IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid covariant_swap_add_of_covariant_add Real.cos_abs spectrum.norm_le_norm_of_mem CStarRing.instNormOneClassOfNontrivial

unitary

Definitions

Name	Category	Theorems
argSelfAdjoint 📖	CompOp	—
openPartialHomeomorph 📖	CompOp	—
path 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuousOn_argSelfAdjoint 📖	mathematical	—	ContinuousOn Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Unitary.argSelfAdjoint Metric.ball Subtype.pseudoMetricSpace Submonoid.one Real instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Unitary.continuousOn_argSelfAdjoint
expUnitary_eq_mul_inv 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule Unitary.argSelfAdjoint Submonoid.mul Star.star Unitary.instStarSubtypeMemSubmonoidUnitary	—	Unitary.expUnitary_eq_mul_inv
isPathConnected_ball 📖	mathematical	Real Real.instLT Real.instZero instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	IsPathConnected Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Metric.ball Subtype.pseudoMetricSpace	—	Unitary.isPathConnected_ball
joined 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Joined instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing	—	Unitary.joined
mem_pathComponentOne_iff 📖	mathematical	—	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing Set Set.instMembership pathComponent instTopologicalSpaceSubtype UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace NormedRing.toSeminormedRing Submonoid.one Submonoid.mul AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule	—	Unitary.mem_pathComponentOne_iff
norm_argSelfAdjoint 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	AddSubgroup AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup Unitary.argSelfAdjoint Real.arccos Real.instSub Real.instOne DivInvMonoid.toDiv Real.instDivInvMonoid Monoid.toNatPow Real.instMonoid	—	Unitary.norm_argSelfAdjoint
norm_argSelfAdjoint_le_pi 📖	mathematical	—	Real Real.instLE Norm.norm AddSubgroup NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing CStarAlgebra.toNormedRing CStarAlgebra.toStarRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup Unitary.argSelfAdjoint Real.pi	—	Unitary.norm_argSelfAdjoint_le_pi
norm_expUnitary_smul_argSelfAdjoint_sub_one_le 📖	mathematical	Real Set Set.instMembership Set.Icc Real.instPreorder Real.instZero Real.instOne Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instLE selfAdjoint.expUnitary CStarAlgebra.toNormedAlgebra NormedStarGroup.to_continuousStar NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CStarRing.to_normedStarGroup CStarAlgebra.toCStarRing CStarAlgebra.toCompleteSpace CStarAlgebra.toStarModule AddSubgroup AddSubgroup.instSetLike selfAdjoint selfAdjoint.instSMulSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instStarRingReal instTrivialStarReal Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField SeminormedRing.toRing NormedRing.toSeminormedRing NormedAlgebra.toAlgebra NormedAlgebra.complexToReal StarModule.complexToReal NormedAddCommGroup.toAddCommGroup SubNegMonoid.toAddMonoid Algebra.toModule Complex Complex.instNormedField Unitary.argSelfAdjoint	—	Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le
norm_sub_eq 📖	mathematical	—	Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing Submonoid.mul Star.star Unitary.instStarSubtypeMemSubmonoidUnitary AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Unitary.norm_sub_eq
norm_sub_one_lt_two_iff 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing	Real Real.instLT Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Complex Set Set.instMembership spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra Complex.instNeg Complex.instOne	—	Unitary.norm_sub_one_lt_two_iff
norm_sub_one_sq_eq 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing IsLeast Real Real.instLE Set.image Complex Complex.re spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra	Monoid.toNatPow Real.instMonoid Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne	—	Unitary.norm_sub_one_sq_eq
spectrum_subset_slitPlane_iff_norm_lt_two 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing	Set Complex Set.instHasSubset spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra Complex.slitPlane Real Real.instLT Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	—	Unitary.spectrum_subset_slitPlane_iff_norm_lt_two
two_mul_one_sub_cos_norm_argSelfAdjoint 📖	mathematical	Real Real.instLT Norm.norm NormedRing.toNorm CStarAlgebra.toNormedRing SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat	Real.instMul Real.instSub Real.instOne Real.cos AddSubgroup AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedAddCommGroup.toNorm AddSubgroup.normedAddCommGroup Unitary.argSelfAdjoint Monoid.toNatPow Real.instMonoid	—	Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
two_mul_one_sub_le_norm_sub_one_sq 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing CStarAlgebra.toNormedRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CStarAlgebra.toStarRing Complex Set Set.instMembership spectrum Complex.instCommSemiring NormedAlgebra.toAlgebra Complex.instNormedField NormedRing.toSeminormedRing CStarAlgebra.toNormedAlgebra	Real Real.instLE Real.instMul instOfNatAtLeastTwo Real.instNatCast Nat.instAtLeastTwoHAddOfNat Real.instSub Real.instOne Complex.re Monoid.toNatPow Real.instMonoid Norm.norm NormedRing.toNorm SubNegMonoid.toSub AddGroup.toSubNegMonoid NormedAddGroup.toAddGroup NormedAddCommGroup.toNormedAddGroup NonUnitalNormedRing.toNormedAddCommGroup NonUnitalCStarAlgebra.toNonUnitalNormedRing CStarAlgebra.toNonUnitalCStarAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Unitary.two_mul_one_sub_le_norm_sub_one_sq

---

← Back to Index