SelfAdjoint

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

Statistics

Metric	Count
Definitions IsSelfAdjoint, IsStarNormal, selfAdjoint, instCommRingSubtypeMemAddSubgroup, instDistribMulActionSubtypeMemAddSubgroupOfStarModule, instDivSubtypeMemAddSubgroup, instField, instInhabitedSubtypeMemAddSubgroup, instIntCastSubtypeMemAddSubgroup, instInvSubtypeMemAddSubgroup, instModuleSubtypeMemAddSubgroupOfStarModule, instMulActionSubtypeMemAddSubgroupOfStarModule, instMulSubtypeMemAddSubgroup, instNNRatCast, instNatCastSubtypeMemAddSubgroup, instOneSubtypeMemAddSubgroup, instPowSubtypeMemAddSubgroupInt, instPowSubtypeMemAddSubgroupNat, instRatCast, instSMulNNRat, instSMulRat, instSMulSubtypeMemAddSubgroupOfStarModule, skewAdjoint, instDistribMulActionSubtypeMemAddSubgroupOfStarModule, instInhabitedSubtypeMemAddSubgroup, instModuleSubtypeMemAddSubgroupOfStarModule, instSMulSubtypeMemAddSubgroupOfStarModule	27
Theorems isStarNormal, isStarNormal_add, isStarNormal_sub, add, add_star_self, all, apply, commute_iff, conj_eq, conjugate, conjugate', conjugate_self, div, intCast, inv, invOf, invOf_iff, inv_iff, inv₀, inv₀_iff, isStarNormal, map, mul, mul_star_self, natCast, neg, nnratCast, ofNat, one, pow, ratCast, smul, smul_iff, smul_mem_skewAdjoint, star_add_self, star_eq, star_iff, star_mul_self, sub, zero, zpow, zpow₀, map, neg, one, one_add, one_sub, smul, star_comm_self, val_inv, zero, isSelfAdjoint_conjugate_iff, isSelfAdjoint_conjugate_iff', isSelfAdjoint, isStarNormal, isSelfAdjoint_conjugate_iff_of_isUnit, isSelfAdjoint_conjugate_iff_of_isUnit', isSelfAdjoint_iff, isSelfAdjoint_map, isSelfAdjoint_smul_of_mem_skewAdjoint, isStarNormal_iff, instNontrivialSubtypeMemAddSubgroup, isSelfAdjoint, isStarNormal, mem_iff, star_val_eq, val_div, val_inv, val_mul, val_nnqsmul, val_nnratCast, val_one, val_pow, val_qsmul, val_ratCast, val_smul, val_zpow, conjugate, conjugate', instIsStarNormalValMemAddSubgroup, isStarNormal_of_mem, mem_iff, smul_mem, star_val_eq, val_smul, star_comm_self'	86
Total	113

CommMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStarNormal 📖	mathematical	—	IsStarNormal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass toMonoid InvolutiveStar.toStar StarMul.toInvolutiveStar	—	mul_comm

Commute

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStarNormal_add 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Distrib.toAdd	—	isStarNormal_iff star_star star_star StarAddMonoid.star_add mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass eq add_add_add_comm
isStarNormal_sub 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	isStarNormal_add neg_right star_neg IsStarNormal.neg sub_eq_add_neg

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddSemigroup.toAdd AddMonoid.toAddSemigroup	—	StarAddMonoid.star_add star_eq
add_star_self 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Star.star	—	StarAddMonoid.star_add star_star add_comm
all 📖	mathematical	—	IsSelfAdjoint	—	TrivialStar.star_trivial
apply 📖	mathematical	IsSelfAdjoint Pi.instStarForall	IsSelfAdjoint	—	Pi.isSelfAdjoint
commute_iff 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar	Commute IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar	—	isSelfAdjoint_iff StarMul.star_mul star_eq Commute.eq
conj_eq 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike starRingEnd	—	star_eq
conjugate 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Semigroup.toMul	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Semigroup.toMul Star.star	—	mul_assoc StarMul.star_mul star_star star_eq
conjugate' 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Semigroup.toMul	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Semigroup.toMul Star.star	—	mul_assoc StarMul.star_mul star_eq star_star
conjugate_self 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Semigroup.toMul	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Semigroup.toMul	—	conjugate
div 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring StarRing.toStarAddMonoid	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring StarRing.toStarAddMonoid DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DivisionSemiring.toGroupWithZero	—	star_div₀ star_eq
intCast 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	star_intCast
inv 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	star_inv star_eq
invOf 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Invertible.invOf MulOne.toOne	—	invOf_iff
invOf_iff 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Invertible.invOf MulOne.toOne	—	isSelfAdjoint_iff star_invOf
inv_iff 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	star_inv
inv₀ 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	star_inv₀ star_eq
inv₀_iff 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	star_inv₀
isStarNormal 📖	mathematical	IsSelfAdjoint	IsStarNormal	—	star_eq
map 📖	mathematical	IsSelfAdjoint	IsSelfAdjoint DFunLike.coe	—	StarHomClass.map_star
mul 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar CommMagma.toMul CommSemigroup.toCommMagma	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar CommMagma.toMul CommSemigroup.toCommMagma	—	star_mul' star_eq
mul_star_self 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Star.star	—	star_star star_mul_self
natCast 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	star_natCast
neg 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	star_neg star_eq
nnratCast 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring StarRing.toStarAddMonoid NNRat.cast DivisionSemiring.toNNRatCast	—	star_nnratCast
ofNat 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid	—	natCast
one 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne MulOne.toOne	—	star_one
pow 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Monoid.toPow	—	star_pow star_eq
ratCast 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing StarRing.toStarAddMonoid DivisionRing.toRatCast	—	star_ratCast
smul 📖	mathematical	IsSelfAdjoint	IsSelfAdjoint	—	StarModule.star_smul star_eq
smul_iff 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass IsUnit	IsSelfAdjoint SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction	—	CanLift.prf instCanLiftUnitsValIsUnit inv_smul_smul Units.ext star_eq smul Units.instStarModule inv
smul_mem_skewAdjoint 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	StarModule.star_smul neg_smul
star_add_self 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Star.star	—	add_comm StarAddMonoid.star_add star_star
star_eq 📖	mathematical	IsSelfAdjoint	Star.star	—	—
star_iff 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar Star.star	—	star_star
star_mul_self 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Star.star	—	StarMul.star_mul star_star
sub 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SubNegMonoid.toSub	—	star_sub star_eq
zero 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass	—	star_zero
zpow 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid DivInvMonoid.toZPow	—	star_zpow star_eq
zpow₀ 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid	—	star_zpow₀ star_eq

IsStarNormal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map 📖	mathematical	—	IsStarNormal DFunLike.coe	—	map_mul StarHomClass.map_star star_comm_self
neg 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	star_neg neg_mul_neg star_comm_self'
one 📖	mathematical	—	IsStarNormal MulOne.toMul MulOneClass.toMulOne InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toOne	—	star_one
one_add 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Distrib.toAdd AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	Commute.isStarNormal_add Commute.one_left one
one_sub 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	Commute.isStarNormal_sub Commute.one_left one
smul 📖	mathematical	—	IsStarNormal	—	Commute.smul_right Commute.smul_left star_comm_self StarModule.star_smul
star_comm_self 📖	mathematical	—	Commute Star.star	—	—
val_inv 📖	mathematical	—	IsStarNormal MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass InvolutiveStar.toStar StarMul.toInvolutiveStar Units.val Units Units.instInv	—	star_comm_self
zero 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	star_zero

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint_conjugate_iff 📖	mathematical	IsUnit	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Star.star	—	mul_assoc StarMul.star_mul star_star star
isSelfAdjoint_conjugate_iff' 📖	mathematical	IsUnit	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Star.star	—	star_star isSelfAdjoint_conjugate_iff star

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint 📖	mathematical	—	IsSelfAdjoint instStarForall	—	—

TrivialStar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isStarNormal 📖	mathematical	—	IsStarNormal InvolutiveStar.toStar StarMul.toInvolutiveStar	—	star_trivial Commute.refl

(root)

Definitions

Name	Category	Theorems
IsSelfAdjoint 📖	MathDef	250 math math: range_cfcₙ_nnreal, imaginaryPart_eq_zero_iff, ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric, CFC.abs_eq_cfc_norm, CFC.sqrt_eq_one_iff', CFC.posPart_one, nnnorm_cfcₙ_nnreal_le_iff, Matrix.IsHermitian.det_abs, CStarAlgebra.nonneg_iff_exists_isSelfAdjoint_and_eq_mul_self, CFC.posPart_natCast, IsSelfAdjoint.star_mul_self, CFC.tendsto_cfc_rpow_sub_one_log, Matrix.IsHermitian.cfc_eq, CFC.sq_sqrt, IsSelfAdjoint.apply, Unitization.real_cfcₙ_eq_cfc_inr, CFC.nnnorm_sqrt, LinearMap.isSelfAdjoint_toContinuousLinearMap_iff, IsSelfAdjoint.sub, CFC.sqrt_rpow, RCLike.is_real_TFAE, Matrix.IsHermitian.isSelfAdjoint, cfc_complex_eq_real, CFC.negPart_algebraMap, cfcₙHom_nnreal_eq_restrict, ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star, IsSelfAdjoint.inv, Continuous.cfc_nnreal', CFC.abs_coe_unitary, RCLike.im_eq_zero_iff_isSelfAdjoint, LE.le.isSelfAdjoint, IsUnit.cfcSqrt, CFC.continuousOn_log, ContinuousOn.cfc_nnreal', IsGreatest.nnnorm_cfc_nnreal, IsSelfAdjoint.add_star_self, IsSelfAdjoint.mul_star_self, CFC.continuousOn_sqrt, IsSelfAdjoint.intCast, Matrix.PosSemidef.det_sqrt, Commute.cfc_real, Matrix.IsHermitian.charpoly_cfc_eq, nnnorm_cfcₙ_nnreal_lt, CFC.sqrt_eq_rpow, Matrix.WithConv.IsIdempotentElem.isSelfAdjoint, CStarAlgebra.nonneg_iff_isSelfAdjoint_and_negPart_eq_zero, cfc_real_eq_nnreal, CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self, IsSelfAdjoint.zpow₀, IsSelfAdjoint.cfc, LinearMap.IsSymmetric.isSelfAdjoint, CFC.posPart_algebraMap_nnreal, CFC.exists_sqrt_of_isSelfAdjoint_of_quasispectrumRestricts, IsSelfAdjoint.exp, CFC.sqrt_eq_one_iff, IsSelfAdjoint.inr, IsSelfAdjoint.commute_iff, CStarAlgebra.norm_posPart_le, IsGreatest.nnnorm_cfcₙ_nnreal, CFC.continuous_abs, continuousOn_cfc_nnreal, IsSelfAdjoint.map, cfc_nnreal_eq_real, cfcₙ_real_eq_complex, IsSelfAdjoint.log, cfcₙ_comp_re, cfc_comp_im, CFC.abs_natCast, CStarAlgebra.isStrictlyPositive_iff_isStrictlyPositive_sqrt_and_eq_sqrt_mul_sqrt, IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, IsSelfAdjoint.cfc_arg, LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star, Matrix.isHermitian_iff_isSelfAdjoint, cfcₙ_comp_im, ContinuousLinearMap.IsIdempotentElem.TFAE, Continuous.cfc_nnreal_of_mem_nhdsSet, Filter.IsIncreasingApproximateUnit.eventually_isSelfAdjoint, IsSelfAdjoint.instNonUnitalContinuousFunctionalCalculus, LinearMap.isSelfAdjoint_iff', IsSelfAdjoint.natCast, Continuous.cfcₙ_nnreal, LinearMap.IsPositive.isSelfAdjoint, Unitization.isSelfAdjoint_inr, cfcHom_real_eq_restrict, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, ContinuousAt.cfcₙ_nnreal, ContinuousOn.cfc_nnreal_of_mem_nhdsSet, CFC.abs_algebraMap, LinearMap.IsSymmetric.isSymmetric_smul_iff, IsSelfAdjoint.inv₀, IsStrictlyPositive.nnrpow, isSelfAdjoint_algebraMap_iff, CFC.monotoneOn_one_sub_one_add_inv_real, IsSelfAdjoint.algebraMap, ContinuousWithinAt.cfcₙ_nnreal, isStarProjection_iff, QuasispectrumRestricts.isSelfAdjoint, IsSelfAdjoint.conj_adjoint, CFC.continuousOn_nnrpow, IsUnit.isSelfAdjoint_conjugate_iff, selfAdjoint.isSelfAdjoint, range_cfcₙ_nnreal_eq_image_cfcₙ_real, Filter.Tendsto.cfcₙ_nnreal, IsSelfAdjoint.inv_iff, IsUnit.cfcNNRpow, ContinuousOn.cfc_nnreal, nnnorm_cfcₙ_nnreal_lt_iff, IsSelfAdjoint.of_nonneg, isSelfAdjoint_sum, ContinuousLinearMap.isSelfAdjoint_iff', isSelfAdjoint_starProjection, nnnorm_cfc_nnreal_lt, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, IsSelfAdjoint.ratCast, IsStrictlyPositive.sqrt, cfcₙ_real_eq_nnreal, cfc_comp_re, nnnorm_cfc_nnreal_le, IsSelfAdjoint.norm_eq_max_norm_posPart_negPart, ContinuousOn.cfcₙ_nnreal_of_mem_nhdsSet, Continuous.cfc_nnreal, nnnorm_cfc_nnreal_le_iff, CFC.sqrt_sq, IsSelfAdjoint.star_iff, CFC.rpow_sqrt_nnreal, ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff, LinearPMap.isSelfAdjoint_def, IsSelfAdjoint.instIsometricContinuousFunctionalCalculus, cfcHom_nnreal_eq_restrict, ContinuousOn.cfcₙ_nnreal', Matrix.IsHermitian.instContinuousFunctionalCalculusIsClosedEmbedding, range_cfc_nnreal, ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint, CFC.abs_ofNat, CFC.negPart_one, Matrix.PosSemidef.inv_sqrt, Matrix.IsHermitian.cfcHom_eq_cfcAux, cfcₙHom_real_eq_restrict, CFC.abs_algebraMap_nnreal, IsStarProjection.isSelfAdjoint, CFC.nnnorm_rpow, Continuous.cfcₙ_nnreal_of_mem_nhdsSet, CStarAlgebra.isStrictlyPositive_iff_isUnit_sqrt_and_eq_sqrt_mul_sqrt, cfc_comp_norm, CFC.abs_intCast, apply_le_nnnorm_cfc_nnreal, range_cfc_nnreal_eq_image_cfc_real, IsSelfAdjoint.of_inr, ContinuousLinearMap.isPositive_def', IsSelfAdjoint.zero, isStarProjection_iff_spectrum_subset_and_isSelfAdjoint, isSelfAdjoint_conjugate_iff_of_isUnit', CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁, CFC.spectrum_abs, IsSelfAdjoint.conj_starProjection, IsSelfAdjoint.add, LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix', CFC.abs_of_mem_unitary, IsSelfAdjoint.star_add_self, CFC.sqrt_eq_cfc, IsSelfAdjoint.inv₀_iff, Filter.Tendsto.cfc_nnreal, IsSelfAdjoint.instContinuousFunctionalCalculus, isStarProjection_iff_quasispectrum_subset_and_isSelfAdjoint, CFC.abs_eq_cfcₙ_norm, continuousOn_cfcₙ_nnreal, CFC.abs_sq, LinearMap.isSelfAdjoint_iff_map_star, LinearMap.isSymmetric_iff_isSelfAdjoint, IsStrictlyPositive.isSelfAdjoint, ContinuousLinearMap.isPositive_iff', CStarAlgebra.isStrictlyPositive_TFAE, CStarAlgebra.isStrictlyPositive_iff_isSelfAdjoint_and_spectrum_pos, isSelfAdjoint_iff, CStarAlgebra.norm_negPart_le, cfcₙ_nnreal_eq_real, CFC.sqrt_algebraMap, CFC.posPart_algebraMap, CFC.sqrt_one, IsSelfAdjoint.pow, IsSelfAdjoint.neg, CFC.nnrpow_eq_cfcₙ_real, IntrinsicStar.StarHomClass.isSelfAdjoint, IsSelfAdjoint.ofNat, IsSelfAdjoint.adjoint_conj, nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts, CFC.negPart_def, CFC.sqrt_rpow_nnreal, nnnorm_cfc_nnreal_lt_iff, IsSelfAdjoint.conjugate_self, IsSelfAdjoint.smul, IsSelfAdjoint.nnratCast, cfc_real_eq_complex, CFC.norm_rpow, isSelfAdjoint_smul_of_mem_skewAdjoint, IsSelfAdjoint.mul, ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, MonotoneOn.nnnorm_cfc, IsSelfAdjoint.zpow, ContinuousOn.cfcₙ_nnreal, CFC.posPart_def, CFC.nnrpow_eq_rpow, CFC.cfcₙ_rpowIntegrand₀₁_eq_cfcₙ_rpowIntegrand₀₁_one, Complex.im_eq_zero_iff_isSelfAdjoint, continuousOn_cfc_nnreal_setProd, CFC.abs_one, CStarAlgebra.nonneg_TFAE, IsSelfAdjoint.invOf, Matrix.isHermitian_diagonal_iff, IsSelfAdjoint.div, StarHomClass.isSelfAdjoint, IsSelfAdjoint.invOf_iff, CFC.isUnit_nnrpow_iff, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, IsSelfAdjoint.all, ContinuousAt.cfc_nnreal, IsSelfAdjoint.one, Pi.isSelfAdjoint, ContinuousWithinAt.cfc_nnreal, IsSelfAdjoint.instNonUnitalIsometricContinuousFunctionalCalculus, ContinuousLinearMap.IsPositive.isSelfAdjoint, nnnorm_cfcₙ_nnreal_le, CFC.sqrt_eq_real_sqrt, apply_le_nnnorm_cfcₙ_nnreal, IsSelfAdjoint.conjugate, IsSelfAdjoint.mono, continuousOn_cfcₙ_nnreal_setProd, CFC.real_exp_eq_normedSpace_exp, CFC.norm_sqrt, CFC.continuousOn_rpow, IsSelfAdjoint.conjugate', MonotoneOn.nnnorm_cfcₙ, CFC.nnnorm_nnrpow, Matrix.PosDef.posDef_sqrt, CFC.norm_nnrpow, Commute.cfcₙ_real, ContinuousLinearMap.IntrinsicStar.isSelfAdjoint_toLinearMap_iff, cfcₙ_complex_eq_real, Matrix.IsHermitian.instContinuousFunctionalCalculus, IsUnit.isSelfAdjoint_conjugate_iff', CStarModule.isSelfAdjoint_inner_self, IsSelfAdjoint.smul_iff, CFC.rpow_eq_cfc_real, isSelfAdjoint_map, Continuous.cfcₙ_nnreal', CFC.isUnit_sqrt_iff, map_isSelfAdjoint, isSelfAdjoint_conjugate_iff_of_isUnit, CFC.rpow_sqrt, IsSelfAdjoint.cfcₙ
IsStarNormal 📖	CompData	91 math math: cfc_realPart, IsStarNormal.instNonUnitalContinuousFunctionalCalculus, IsStarNormal.one_sub, cfc_im_id, CFC.monotoneOn_one_sub_one_add_inv, CFC.monotone_nnrpow, CFC.tendsto_cfc_rpow_sub_one_log, Unitization.real_cfcₙ_eq_cfc_inr, skewAdjoint.isStarNormal_of_mem, ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint, cfc_complex_eq_real, Unitization.sqrt_inr, skewAdjoint.instIsStarNormalValMemAddSubgroup, IsStarNormal.cfcₙ_map, cfcₙ_re_id, isStarNormal_iff, IsStarNormal.neg, IsStarNormal.val_inv, IsStarNormal.zero, cfcₙ_real_eq_complex, cfcₙ_comp_re, cfc_comp_im, IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, IsSelfAdjoint.cfc_arg, cfcₙ_comp_im, ContinuousLinearMap.IsIdempotentElem.TFAE, Commute.isStarNormal_add, cfcHom_real_eq_restrict, TrivialStar.isStarNormal, CFC.log_monotoneOn, CFC.monotone_rpow, inr_comp_cfcₙHom_eq_cfcₙAux, CFC.monotoneOn_one_sub_one_add_inv_real, Unitary.instIsStarNormal, IsSelfAdjoint.isStarNormal, Commute.isStarNormal_sub, QuaternionAlgebra.instIsStarNormal, isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts, cfcₙ_imaginaryPart, CFC.rpow_le_rpow, cfc_comp_re, Unitary.coe_isStarNormal, selfAdjoint.star_coe_unitarySelfAddISMul, CStarAlgebra.rpow_neg_one_le_rpow_neg_one, Quaternion.instIsStarNormal, cfcₙ_im_id, Unitization.nnreal_cfcₙ_eq_cfc_inr, IsStarNormal.map, cfcₙHom_real_eq_restrict, CFC.nnrpow_le_nnrpow, IsStarNormal.instContinuousFunctionalCalculus, IsStarNormal.one, IsStarNormal.cfc_map, Unitization.instIsStarNormal, IsStarNormal.star, CStarAlgebra.rpow_neg_one_le_one, ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal, isStarProjection_iff_spectrum_subset_and_isStarNormal, unitary_iff_isStarNormal_and_spectrum_subset_unitary, CFC.monotone_sqrt, norm_cfcₙ_one_sub_one_add_inv_lt_one, IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus, isStarProjection_iff_isIdempotentElem_and_isStarNormal, Unitization.complex_cfcₙ_eq_cfc_inr, CFC.log_le_log, CFC.sqrt_le_sqrt, cfc_re_id, IsStarNormal.smul, IsStarNormal.of_inr, isStarNormal_of_mem_unitary, IsSelfAdjoint.self_add_I_smul_cfcSqrt_sub_sq_mem_unitary, cfcₙ_realPart, cfc_real_eq_complex, ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal, IsStarNormal.one_add, IsStarProjection.isStarNormal, selfAdjoint.isStarNormal, CFC.monotoneOn_cfcₙ_rpowIntegrand₀₁, IsStarNormal.instIsometricContinuousFunctionalCalculus, Unitary.argSelfAdjoint_coe, CommMonoid.isStarNormal, cfcHom_eq_of_isStarNormal, mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one, CFC.conjugate_rpow_neg_one_half, le_iff_norm_sqrt_mul_rpow, cfcₙ_complex_eq_real, Unitization.isStarNormal_inr, isStarNormal_iff_commute_realPart_imaginaryPart, le_iff_norm_sqrt_mul_sqrt_inv, cfc_imaginaryPart, isStarProjection_iff_quasispectrum_subset_and_isStarNormal
selfAdjoint 📖	CompOp	124 math math: cfc_realPart, Unitary.openPartialHomeomorph_source, continuous_decomposeProdAdjoint, StarModule.decomposeProdAdjointL_symm_apply, StarModule.selfAdjointPart_add_skewAdjointPart, unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, imaginaryPart_eq_zero_iff, Commute.realPart_imaginaryPart, Complex.coe_realPart, quasispectrum_imaginaryPart, selfAdjoint.val_div, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, cfc_im_id, realPart_idem, realPart_ofReal, Unitary.mem_pathComponentOne_iff, imaginaryPart_I_smul, selfAdjoint.expUnitaryPathToOne_apply, Unitary.continuousOn_argSelfAdjoint, selfAdjoint.norm_sq_expUnitary_sub_one, selfAdjoint.val_mul, selfAdjointPart_comp_subtype_skewAdjoint, IsSelfAdjoint.selfAdjointPart_apply, StarModule.decomposeProdAdjointL_apply, selfAdjoint.val_one, selfAdjointPart_comp_subtype_selfAdjoint, Unitary.openPartialHomeomorph_symm_apply, selfAdjoint.instNontrivialSubtypeMemAddSubgroup, selfAdjoint.imaginaryPart_coe, selfAdjoint.val_zpow, cfcₙ_re_id, continuous_decomposeProdAdjoint_symm, realPart.norm_le, selfAdjoint.expUnitary_zero, LinearMap.IsSymmetric.coe_toSelfAdjoint, realPart_add_I_smul_imaginaryPart, selfAdjoint.continuous_expUnitary, ComplexStarModule.ext_iff, selfAdjoint.unitarySelfAddISMul_coe, quasispectrum_imaginaryPart', selfAdjoint.star_val_eq, StarModule.decomposeProdAdjoint_symm_apply, cfcₙ_comp_re, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, cfc_comp_im, realPart_one, LinearMap.IsSymmetric.toSelfAdjoint_apply, cfcₙ_comp_im, Complex.selfAdjointEquiv_apply, CStarAlgebra.linear_combination_nonneg, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, star_mul_self_add_self_mul_star, imaginaryPart.norm_le, realPart_comp_subtype_selfAdjoint, spectrum_imaginaryPart, unitary.norm_argSelfAdjoint, skewAdjoint.negISMul_apply_coe, imaginaryPart_realPart, imaginaryPart_eq_neg_I_smul_skewAdjointPart, selfAdjoint.isSelfAdjoint, span_selfAdjoint, realPart_I_smul, selfAdjoint.realPart_unitarySelfAddISMul, cfcₙ_imaginaryPart, imaginaryPart_apply_coe, Unitary.openPartialHomeomorph_target, cfc_comp_re, imaginaryPart_comp_subtype_selfAdjoint, selfAdjoint.val_inv, selfAdjoint.val_smul, realPart_surjective, selfAdjoint.star_coe_unitarySelfAddISMul, cfcₙ_im_id, quasispectrum_realPart, imaginaryPart_surjective, selfAdjoint.val_pow, selfAdjoint.realPart_coe, continuous_selfAdjointPart, selfAdjoint.val_qsmul, selfAdjointPartL_apply_coe, Complex.coe_selfAdjointEquiv, imaginaryPart_ofReal, Commute.expUnitary_add, IsSelfAdjoint.coe_selfAdjointPart_apply, selfAdjoint.val_ratCast, Complex.selfAdjointEquiv_symm_apply, selfAdjointPart_apply_coe, ker_imaginaryPart, realPart_imaginaryPart, selfAdjoint.mem_iff, skewAdjointPart_eq_I_smul_imaginaryPart, selfAdjoint.val_nnratCast, selfAdjoint.val_re_map_spectrum, star_mul_self_sub_self_mul_star, imaginaryPart_imaginaryPart, quasispectrum_realPart', cfc_re_id, imaginaryPart_smul, cfcₙ_realPart, Unitary.norm_argSelfAdjoint, realPart_apply_coe, spectrum_realPart, spectrum_imaginaryPart', IsSelfAdjoint.coe_realPart, realPart_smul, unitary.norm_argSelfAdjoint_le_pi, Unitary.norm_argSelfAdjoint_le_pi, selfAdjoint.isStarNormal, spectrum_realPart', Unitary.openPartialHomeomorph_apply, Unitary.argSelfAdjoint_coe, skewAdjoint.I_smul_neg_I, IsSelfAdjoint.imaginaryPart, unitary.mem_pathComponentOne_iff, mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one, Unitary.path_apply, unitary.two_mul_one_sub_cos_norm_argSelfAdjoint, selfAdjoint.expUnitary_coe, selfAdjoint.val_nnqsmul, StarModule.decomposeProdAdjoint_apply, isStarNormal_iff_commute_realPart_imaginaryPart, unitary.continuousOn_argSelfAdjoint, cfc_imaginaryPart, Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint
skewAdjoint 📖	CompOp	25 math math: continuous_decomposeProdAdjoint, StarModule.decomposeProdAdjointL_symm_apply, StarModule.selfAdjointPart_add_skewAdjointPart, IsSelfAdjoint.smul_mem_skewAdjoint, StarModule.decomposeProdAdjointL_apply, skewAdjoint.mem_iff, skewAdjoint.val_smul, skewAdjoint.instIsStarNormalValMemAddSubgroup, continuous_decomposeProdAdjoint_symm, IsSelfAdjoint.skewAdjointPart_apply, StarModule.decomposeProdAdjoint_symm_apply, skewAdjoint.negISMul_apply_coe, imaginaryPart_eq_neg_I_smul_skewAdjointPart, skewAdjointPart_comp_subtype_selfAdjoint, skewAdjoint.star_val_eq, skewAdjointPart_apply_coe, skewAdjoint.conjugate', skewAdjointPartL_apply_coe, skewAdjointPart_eq_I_smul_imaginaryPart, skewAdjoint.conjugate, skewAdjoint.smul_mem, skewAdjoint.I_smul_neg_I, skewAdjointPart_comp_subtype_skewAdjoint, continuous_skewAdjointPart, StarModule.decomposeProdAdjoint_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint_conjugate_iff_of_isUnit 📖	mathematical	IsUnit	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Star.star	—	IsUnit.isSelfAdjoint_conjugate_iff
isSelfAdjoint_conjugate_iff_of_isUnit' 📖	mathematical	IsUnit	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass Star.star	—	IsUnit.isSelfAdjoint_conjugate_iff'
isSelfAdjoint_iff 📖	mathematical	—	IsSelfAdjoint Star.star	—	—
isSelfAdjoint_map 📖	mathematical	—	IsSelfAdjoint DFunLike.coe	—	IsSelfAdjoint.map IsSelfAdjoint.all
isSelfAdjoint_smul_of_mem_skewAdjoint 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid	—	StarModule.star_smul neg_smul_neg
isStarNormal_iff 📖	mathematical	—	IsStarNormal Commute Star.star	—	—
star_comm_self' 📖	mathematical	—	Star.star	—	IsStarNormal.star_comm_self

selfAdjoint

Definitions

Name	Category	Theorems
instCommRingSubtypeMemAddSubgroup 📖	CompOp	3 math math: Complex.selfAdjointEquiv_apply, Complex.coe_selfAdjointEquiv, Complex.selfAdjointEquiv_symm_apply
instDistribMulActionSubtypeMemAddSubgroupOfStarModule 📖	CompOp	—
instDivSubtypeMemAddSubgroup 📖	CompOp	1 math math: val_div
instField 📖	CompOp	—
instInhabitedSubtypeMemAddSubgroup 📖	CompOp	—
instIntCastSubtypeMemAddSubgroup 📖	CompOp	—
instInvSubtypeMemAddSubgroup 📖	CompOp	1 math math: val_inv
instModuleSubtypeMemAddSubgroupOfStarModule 📖	CompOp	78 math math: cfc_realPart, continuous_decomposeProdAdjoint, StarModule.decomposeProdAdjointL_symm_apply, StarModule.selfAdjointPart_add_skewAdjointPart, imaginaryPart_eq_zero_iff, Commute.realPart_imaginaryPart, Complex.coe_realPart, quasispectrum_imaginaryPart, cfc_im_id, realPart_idem, realPart_ofReal, imaginaryPart_I_smul, selfAdjointPart_comp_subtype_skewAdjoint, IsSelfAdjoint.selfAdjointPart_apply, StarModule.decomposeProdAdjointL_apply, selfAdjointPart_comp_subtype_selfAdjoint, imaginaryPart_coe, cfcₙ_re_id, continuous_decomposeProdAdjoint_symm, realPart.norm_le, realPart_add_I_smul_imaginaryPart, ComplexStarModule.ext_iff, quasispectrum_imaginaryPart', StarModule.decomposeProdAdjoint_symm_apply, cfcₙ_comp_re, star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, cfc_comp_im, realPart_one, cfcₙ_comp_im, Complex.selfAdjointEquiv_apply, CStarAlgebra.linear_combination_nonneg, CStarAlgebra.norm_smul_two_inv_smul_add_four_unitary, star_mul_self_add_self_mul_star, imaginaryPart.norm_le, realPart_comp_subtype_selfAdjoint, spectrum_imaginaryPart, skewAdjoint.negISMul_apply_coe, imaginaryPart_realPart, imaginaryPart_eq_neg_I_smul_skewAdjointPart, realPart_I_smul, realPart_unitarySelfAddISMul, cfcₙ_imaginaryPart, imaginaryPart_apply_coe, cfc_comp_re, imaginaryPart_comp_subtype_selfAdjoint, realPart_surjective, cfcₙ_im_id, quasispectrum_realPart, imaginaryPart_surjective, realPart_coe, continuous_selfAdjointPart, selfAdjointPartL_apply_coe, Complex.coe_selfAdjointEquiv, imaginaryPart_ofReal, IsSelfAdjoint.coe_selfAdjointPart_apply, Complex.selfAdjointEquiv_symm_apply, selfAdjointPart_apply_coe, ker_imaginaryPart, realPart_imaginaryPart, skewAdjointPart_eq_I_smul_imaginaryPart, star_mul_self_sub_self_mul_star, imaginaryPart_imaginaryPart, quasispectrum_realPart', cfc_re_id, imaginaryPart_smul, cfcₙ_realPart, realPart_apply_coe, spectrum_realPart, spectrum_imaginaryPart', IsSelfAdjoint.coe_realPart, realPart_smul, spectrum_realPart', skewAdjoint.I_smul_neg_I, IsSelfAdjoint.imaginaryPart, mem_unitary_iff_isStarNormal_and_realPart_sq_add_imaginaryPart_sq_eq_one, StarModule.decomposeProdAdjoint_apply, isStarNormal_iff_commute_realPart_imaginaryPart, cfc_imaginaryPart
instMulActionSubtypeMemAddSubgroupOfStarModule 📖	CompOp	—
instMulSubtypeMemAddSubgroup 📖	CompOp	1 math math: val_mul
instNNRatCast 📖	CompOp	1 math math: val_nnratCast
instNatCastSubtypeMemAddSubgroup 📖	CompOp	—
instOneSubtypeMemAddSubgroup 📖	CompOp	2 math math: val_one, realPart_one
instPowSubtypeMemAddSubgroupInt 📖	CompOp	1 math math: val_zpow
instPowSubtypeMemAddSubgroupNat 📖	CompOp	1 math math: val_pow
instRatCast 📖	CompOp	1 math math: val_ratCast
instSMulNNRat 📖	CompOp	1 math math: val_nnqsmul
instSMulRat 📖	CompOp	1 math math: val_qsmul
instSMulSubtypeMemAddSubgroupOfStarModule 📖	CompOp	7 math math: unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le, expUnitaryPathToOne_apply, val_smul, imaginaryPart_smul, realPart_smul, Unitary.path_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNontrivialSubtypeMemAddSubgroup 📖	mathematical	—	Nontrivial AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	zero_ne_one NeZero.one
isSelfAdjoint 📖	mathematical	—	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint	—	star_val_eq
isStarNormal 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint	—	IsSelfAdjoint.isStarNormal Subtype.prop
mem_iff 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid	—	AddSubgroup.mem_carrier
star_val_eq 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint	—	Subtype.prop
val_div 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instDivSubtypeMemAddSubgroup DivInvMonoid.toDiv DivisionRing.toDivInvMonoid	—	—
val_inv 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instInvSubtypeMemAddSubgroup InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Field.toSemifield	—	—
val_mul 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring instMulSubtypeMemAddSubgroup Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
val_nnqsmul 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NNRat instSMulNNRat NNRat.smulDivisionSemiring Semifield.toDivisionSemiring Field.toSemifield	—	—
val_nnratCast 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing NNRat.cast instNNRatCast DivisionRing.toNNRatCast	—	—
val_one 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instOneSubtypeMemAddSubgroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne	—	—
val_pow 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instPowSubtypeMemAddSubgroupNat Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring	—	—
val_qsmul 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instSMulRat Rat.smulDivisionRing	—	—
val_ratCast 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instRatCast DivisionRing.toRatCast	—	—
val_smul 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint instSMulSubtypeMemAddSubgroupOfStarModule	—	—
val_zpow 📖	mathematical	—	AddSubgroup AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SetLike.instMembership AddSubgroup.instSetLike selfAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing instPowSubtypeMemAddSubgroupInt DivInvMonoid.toZPow DivisionRing.toDivInvMonoid	—	—

skewAdjoint

Definitions

Name	Category	Theorems
instDistribMulActionSubtypeMemAddSubgroupOfStarModule 📖	CompOp	—
instInhabitedSubtypeMemAddSubgroup 📖	CompOp	—
instModuleSubtypeMemAddSubgroupOfStarModule 📖	CompOp	17 math math: continuous_decomposeProdAdjoint, StarModule.decomposeProdAdjointL_symm_apply, StarModule.selfAdjointPart_add_skewAdjointPart, StarModule.decomposeProdAdjointL_apply, continuous_decomposeProdAdjoint_symm, IsSelfAdjoint.skewAdjointPart_apply, StarModule.decomposeProdAdjoint_symm_apply, negISMul_apply_coe, imaginaryPart_eq_neg_I_smul_skewAdjointPart, skewAdjointPart_comp_subtype_selfAdjoint, skewAdjointPart_apply_coe, skewAdjointPartL_apply_coe, skewAdjointPart_eq_I_smul_imaginaryPart, I_smul_neg_I, skewAdjointPart_comp_subtype_skewAdjoint, continuous_skewAdjointPart, StarModule.decomposeProdAdjoint_apply
instSMulSubtypeMemAddSubgroupOfStarModule 📖	CompOp	1 math math: val_smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
conjugate 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	mul_assoc StarMul.star_mul star_star mem_iff mul_neg neg_mul
conjugate' 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid	—	mul_assoc StarMul.star_mul mem_iff mul_neg star_star neg_mul
instIsStarNormalValMemAddSubgroup 📖	mathematical	—	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint	—	isStarNormal_of_mem SetLike.coe_mem
isStarNormal_of_mem 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup Ring.toAddCommGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	IsStarNormal Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	—
mem_iff 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	AddSubgroup.mem_carrier
smul_mem 📖	mathematical	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_iff StarModule.star_smul TrivialStar.star_trivial smul_neg
star_val_eq 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Subtype.prop
val_smul 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint instSMulSubtypeMemAddSubgroupOfStarModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	—

---

← Back to Index