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`, `inv₀`, `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'`	82
Total	109

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.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` `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`	`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` 📖	—	`IsSelfAdjoint` `Pi.instStarForall`	—	—	`Pi.isSelfAdjoint`
`commute_iff` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar`	`Commute`	—	`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` `RingHom.instFunLike` `starRingEnd`	—	`star_eq`
`conjugate` 📖	mathematical	`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`	`Star.star`	—	`mul_assoc` `StarMul.star_mul` `star_eq` `star_star`
`conjugate_self` 📖	—	`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`	`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`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`star_inv` `star_eq`
`inv₀` 📖	mathematical	`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`
`isStarNormal` 📖	mathematical	`IsSelfAdjoint`	`IsStarNormal`	—	`star_eq`
`map` 📖	mathematical	`IsSelfAdjoint`	`DFunLike.coe`	—	`StarHomClass.map_star`
`mul` 📖	—	`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` `Semiring.toNonAssocSemiring` `StarRing.toStarAddMonoid` `AddMonoidWithOne.toNatCast` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	—	`star_natCast`
`neg` 📖	mathematical	`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` `Semiring.toNonAssocSemiring` `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`	`Monoid.toNatPow`	—	`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` 📖	—	`IsSelfAdjoint`	—	—	`StarModule.star_smul` `star_eq`
`smul_iff` 📖	mathematical	`IsSelfAdjoint` `InvolutiveStar.toStar` `StarMul.toInvolutiveStar` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `IsUnit`	`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`	`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`
`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`	`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`	`DivInvMonoid.toZPow`	—	`star_zpow` `star_eq`
`zpow₀` 📖	mathematical	`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	203 math math: `ContinuousLinearMap.isSelfAdjoint_iff_isSymmetric`, `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`, `Unitization.real_cfcₙ_eq_cfc_inr`, `CFC.nnnorm_sqrt`, `LinearMap.isSelfAdjoint_toContinuousLinearMap_iff`, `CFC.sqrt_rpow`, `Matrix.PosSemidef.sqrt_eq_zero_iff`, `RCLike.is_real_TFAE`, `Matrix.IsHermitian.isSelfAdjoint`, `isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts`, `CFC.negPart_algebraMap`, `cfcₙHom_nnreal_eq_restrict`, `Continuous.cfc_nnreal'`, `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`, `CStarAlgebra.nonneg_iff_isSelfAdjoint_and_negPart_eq_zero`, `cfc_real_eq_nnreal`, `Matrix.PosSemidef.posSemidef_sqrt`, `CStarAlgebra.isStrictlyPositive_iff_exists_isUnit_and_isSelfAdjoint_and_eq_mul_self`, `IsSelfAdjoint.cfc`, `LinearMap.IsSymmetric.isSelfAdjoint`, `CFC.posPart_algebraMap_nnreal`, `Matrix.PosSemidef.sqrt_eq_one_iff`, `Matrix.PosSemidef.sqrt_sq`, `CFC.sqrt_eq_one_iff`, `CStarAlgebra.norm_posPart_le`, `IsGreatest.nnnorm_cfcₙ_nnreal`, `Matrix.PosSemidef.eq_sqrt_iff_sq_eq`, `CFC.continuous_abs`, `continuousOn_cfc_nnreal`, `cfc_nnreal_eq_real`, `IsSelfAdjoint.log`, `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`, `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`, `Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff`, `ContinuousAt.cfcₙ_nnreal`, `nonneg_iff_isSelfAdjoint_and_spectrumRestricts`, `ContinuousOn.cfc_nnreal_of_mem_nhdsSet`, `CFC.abs_algebraMap`, `LinearMap.IsSymmetric.isSymmetric_smul_iff`, `IsStrictlyPositive.nnrpow`, `isSelfAdjoint_algebraMap_iff`, `CFC.monotoneOn_one_sub_one_add_inv_real`, `ContinuousWithinAt.cfcₙ_nnreal`, `isStarProjection_iff`, `QuasispectrumRestricts.isSelfAdjoint`, `CFC.continuousOn_nnrpow`, `IsUnit.isSelfAdjoint_conjugate_iff`, `selfAdjoint.isSelfAdjoint`, `range_cfcₙ_nnreal_eq_image_cfcₙ_real`, `Filter.Tendsto.cfcₙ_nnreal`, `IsUnit.cfcNNRpow`, `SpectrumRestricts.isSelfAdjoint`, `ContinuousOn.cfc_nnreal`, `nnnorm_cfcₙ_nnreal_lt_iff`, `IsSelfAdjoint.of_nonneg`, `ContinuousLinearMap.isSelfAdjoint_iff'`, `isSelfAdjoint_starProjection`, `nnnorm_cfc_nnreal_lt`, `isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts`, `IsSelfAdjoint.ratCast`, `IsStrictlyPositive.sqrt`, `Matrix.PosSemidef.isUnit_sqrt_iff`, `cfcₙ_real_eq_nnreal`, `nnnorm_cfc_nnreal_le`, `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`, `Matrix.PosSemidef.sq_sqrt`, `ContinuousOn.cfcₙ_nnreal'`, `ContinuousLinearMap.IsIdempotentElem.isPositive_iff_isSelfAdjoint`, `CFC.abs_ofNat`, `CFC.negPart_one`, `Matrix.PosSemidef.inv_sqrt`, `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`, `ContinuousLinearMap.isPositive_def'`, `IsSelfAdjoint.zero`, `isSelfAdjoint_conjugate_iff_of_isUnit'`, `CFC.exists_measure_nnrpow_eq_integral_cfcₙ_rpowIntegrand₀₁`, `CFC.spectrum_abs`, `LinearMap.IntrinsicStar.isSelfAdjoint_iff_toMatrix'`, `IsSelfAdjoint.star_add_self`, `CFC.sqrt_eq_cfc`, `Filter.Tendsto.cfc_nnreal`, `IsSelfAdjoint.instContinuousFunctionalCalculus`, `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`, `CFC.nnrpow_eq_cfcₙ_real`, `IntrinsicStar.StarHomClass.isSelfAdjoint`, `IsSelfAdjoint.ofNat`, `nonneg_iff_isSelfAdjoint_and_quasispectrumRestricts`, `CFC.negPart_def`, `CFC.sqrt_rpow_nnreal`, `nnnorm_cfc_nnreal_lt_iff`, `IsSelfAdjoint.nnratCast`, `CFC.norm_rpow`, `isSelfAdjoint_smul_of_mem_skewAdjoint`, `ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal`, `MonotoneOn.nnnorm_cfc`, `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`, `Matrix.PosSemidef.sqrt_mul_self`, `Matrix.isHermitian_diagonal_iff`, `StarHomClass.isSelfAdjoint`, `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`, `continuousOn_cfcₙ_nnreal_setProd`, `CFC.norm_sqrt`, `CFC.continuousOn_rpow`, `MonotoneOn.nnnorm_cfcₙ`, `CFC.nnnorm_nnrpow`, `Matrix.PosDef.posDef_sqrt`, `CFC.norm_nnrpow`, `Commute.cfcₙ_real`, `Matrix.IsHermitian.instContinuousFunctionalCalculus`, `IsUnit.isSelfAdjoint_conjugate_iff'`, `CStarModule.isSelfAdjoint_inner_self`, `Matrix.PosSemidef.sqrt_eq_iff_eq_sq`, `CFC.rpow_eq_cfc_real`, `isSelfAdjoint_map`, `Continuous.cfcₙ_nnreal'`, `CFC.isUnit_sqrt_iff`, `isSelfAdjoint_conjugate_iff_of_isUnit`, `CFC.rpow_sqrt`, `IsSelfAdjoint.cfcₙ`
`IsStarNormal` 📖	CompData	53 math math: `IsStarNormal.instNonUnitalContinuousFunctionalCalculus`, `IsStarNormal.one_sub`, `skewAdjoint.isStarNormal_of_mem`, `ContinuousLinearMap.isStarNormal_iff_norm_eq_adjoint`, `cfc_complex_eq_real`, `isSelfAdjoint_iff_isStarNormal_and_spectrumRestricts`, `skewAdjoint.instIsStarNormalValMemAddSubgroup`, `IsStarNormal.cfcₙ_map`, `isStarNormal_iff`, `IsStarNormal.neg`, `IsStarNormal.val_inv`, `IsStarNormal.zero`, `cfcₙ_real_eq_complex`, `IsIdempotentElem.isSelfAdjoint_iff_isStarNormal`, `IsSelfAdjoint.cfc_arg`, `ContinuousLinearMap.IsIdempotentElem.TFAE`, `Commute.isStarNormal_add`, `cfcHom_real_eq_restrict`, `TrivialStar.isStarNormal`, `inr_comp_cfcₙHom_eq_cfcₙAux`, `Unitary.instIsStarNormal`, `IsSelfAdjoint.isStarNormal`, `Commute.isStarNormal_sub`, `QuaternionAlgebra.instIsStarNormal`, `isSelfAdjoint_iff_isStarNormal_and_quasispectrumRestricts`, `Unitary.coe_isStarNormal`, `Quaternion.instIsStarNormal`, `IsStarNormal.map`, `cfcₙHom_real_eq_restrict`, `IsStarNormal.instContinuousFunctionalCalculus`, `IsStarNormal.one`, `IsStarNormal.cfc_map`, `Unitization.instIsStarNormal`, `IsStarNormal.star`, `ContinuousLinearMap.isStarProjection_iff_isIdempotentElem_and_isStarNormal`, `unitary_iff_isStarNormal_and_spectrum_subset_unitary`, `IsStarNormal.instNonUnitalIsometricContinuousFunctionalCalculus`, `isStarProjection_iff_isIdempotentElem_and_isStarNormal`, `Unitization.complex_cfcₙ_eq_cfc_inr`, `IsStarNormal.smul`, `IsStarNormal.of_inr`, `isStarNormal_of_mem_unitary`, `cfc_real_eq_complex`, `ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal`, `IsStarNormal.one_add`, `IsStarProjection.isStarNormal`, `selfAdjoint.isStarNormal`, `IsStarNormal.instIsometricContinuousFunctionalCalculus`, `Unitary.argSelfAdjoint_coe`, `CommMonoid.isStarNormal`, `cfcHom_eq_of_isStarNormal`, `cfcₙ_complex_eq_real`, `Unitization.isStarNormal_inr`
`selfAdjoint` 📖	CompOp	90 math math: `Unitary.openPartialHomeomorph_source`, `continuous_decomposeProdAdjoint`, `StarModule.decomposeProdAdjointL_symm_apply`, `StarModule.selfAdjointPart_add_skewAdjointPart`, `unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le`, `Complex.coe_realPart`, `selfAdjoint.val_div`, `Unitary.norm_expUnitary_smul_argSelfAdjoint_sub_one_le`, `realPart_idem`, `realPart_ofReal`, `Unitary.mem_pathComponentOne_iff`, `imaginaryPart_I_smul`, `selfAdjoint.expUnitaryPathToOne_apply`, `Unitary.continuousOn_argSelfAdjoint`, `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`, `continuous_decomposeProdAdjoint_symm`, `realPart.norm_le`, `selfAdjoint.expUnitary_zero`, `LinearMap.IsSymmetric.coe_toSelfAdjoint`, `realPart_add_I_smul_imaginaryPart`, `selfAdjoint.continuous_expUnitary`, `selfAdjoint.star_val_eq`, `StarModule.decomposeProdAdjoint_symm_apply`, `LinearMap.IsSymmetric.toSelfAdjoint_apply`, `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`, `unitary.norm_argSelfAdjoint`, `skewAdjoint.negISMul_apply_coe`, `imaginaryPart_realPart`, `imaginaryPart_eq_neg_I_smul_skewAdjointPart`, `selfAdjoint.isSelfAdjoint`, `span_selfAdjoint`, `realPart_I_smul`, `imaginaryPart_apply_coe`, `Unitary.openPartialHomeomorph_target`, `imaginaryPart_comp_subtype_selfAdjoint`, `selfAdjoint.val_inv`, `selfAdjoint.val_smul`, `realPart_surjective`, `imaginaryPart_surjective`, `selfAdjoint.val_pow`, `selfAdjoint.realPart_coe`, `continuous_selfAdjointPart`, `selfAdjoint.val_qsmul`, `selfAdjointPartL_apply_coe`, `Complex.coe_selfAdjointEquiv`, `imaginaryPart_ofReal`, `IsSelfAdjoint.coe_selfAdjointPart_apply`, `selfAdjoint.val_ratCast`, `Complex.selfAdjointEquiv_symm_apply`, `selfAdjointPart_apply_coe`, `realPart_imaginaryPart`, `selfAdjoint.mem_iff`, `skewAdjointPart_eq_I_smul_imaginaryPart`, `selfAdjoint.val_nnratCast`, `selfAdjoint.val_re_map_spectrum`, `imaginaryPart_imaginaryPart`, `imaginaryPart_smul`, `Unitary.norm_argSelfAdjoint`, `realPart_apply_coe`, `IsSelfAdjoint.coe_realPart`, `realPart_smul`, `unitary.norm_argSelfAdjoint_le_pi`, `Unitary.norm_argSelfAdjoint_le_pi`, `selfAdjoint.isStarNormal`, `Unitary.openPartialHomeomorph_apply`, `Unitary.argSelfAdjoint_coe`, `skewAdjoint.I_smul_neg_I`, `IsSelfAdjoint.imaginaryPart`, `unitary.mem_pathComponentOne_iff`, `Unitary.path_apply`, `unitary.two_mul_one_sub_cos_norm_argSelfAdjoint`, `selfAdjoint.expUnitary_coe`, `selfAdjoint.val_nnqsmul`, `StarModule.decomposeProdAdjoint_apply`, `unitary.continuousOn_argSelfAdjoint`, `Unitary.two_mul_one_sub_cos_norm_argSelfAdjoint`
`skewAdjoint` 📖	CompOp	21 math math: `continuous_decomposeProdAdjoint`, `StarModule.decomposeProdAdjointL_symm_apply`, `StarModule.selfAdjointPart_add_skewAdjointPart`, `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`, `skewAdjointPartL_apply_coe`, `skewAdjointPart_eq_I_smul_imaginaryPart`, `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` `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	49 math math: `continuous_decomposeProdAdjoint`, `StarModule.decomposeProdAdjointL_symm_apply`, `StarModule.selfAdjointPart_add_skewAdjointPart`, `Complex.coe_realPart`, `realPart_idem`, `realPart_ofReal`, `imaginaryPart_I_smul`, `selfAdjointPart_comp_subtype_skewAdjoint`, `IsSelfAdjoint.selfAdjointPart_apply`, `StarModule.decomposeProdAdjointL_apply`, `selfAdjointPart_comp_subtype_selfAdjoint`, `imaginaryPart_coe`, `continuous_decomposeProdAdjoint_symm`, `realPart.norm_le`, `realPart_add_I_smul_imaginaryPart`, `StarModule.decomposeProdAdjoint_symm_apply`, `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`, `skewAdjoint.negISMul_apply_coe`, `imaginaryPart_realPart`, `imaginaryPart_eq_neg_I_smul_skewAdjointPart`, `realPart_I_smul`, `realPart_unitarySelfAddISMul`, `imaginaryPart_apply_coe`, `imaginaryPart_comp_subtype_selfAdjoint`, `realPart_surjective`, `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`, `realPart_imaginaryPart`, `skewAdjointPart_eq_I_smul_imaginaryPart`, `imaginaryPart_imaginaryPart`, `imaginaryPart_smul`, `realPart_apply_coe`, `IsSelfAdjoint.coe_realPart`, `realPart_smul`, `skewAdjoint.I_smul_neg_I`, `IsSelfAdjoint.imaginaryPart`, `StarModule.decomposeProdAdjoint_apply`
`instMulActionSubtypeMemAddSubgroupOfStarModule` 📖	CompOp	—
`instMulSubtypeMemAddSubgroup` 📖	CompOp	1 math math: `val_mul`
`instNNRatCast` 📖	CompOp	1 math math: `val_nnratCast`
`instNatCastSubtypeMemAddSubgroup` 📖	CompOp	—
`instOneSubtypeMemAddSubgroup` 📖	CompOp	1 math math: `val_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.toNatPow` `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`	`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`	`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` `InvolutiveStar.toStar` `StarAddMonoid.toInvolutiveStar` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid`	—	—
`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`	`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