Basic

📁 Source: Mathlib/Analysis/CStarAlgebra/Basic.lean

Statistics

Metric	Count
Definitions CStarRing, NormedStarGroup, starRing', toNormedAlgebra, instNormedSpaceSubtypeMemAddSubgroupSelfAdjointOfTrivialStarOfStarModule, starNormedAddGroupHom, starₗᵢ	7
Theorems instMulOpposite, instNormOneClassOfNontrivial, mul_star_self_eq_zero_iff, mul_star_self_ne_zero_iff, nnnorm_self_mul_star, nnnorm_star_mul_self, norm_coe_unitary, norm_coe_unitary_mul, norm_mem_unitary_mul, norm_mul_coe_unitary, norm_mul_mem_unitary, norm_mul_self_le, norm_of_mem_unitary, norm_one, norm_self_mul_star, norm_star_mul_self, norm_star_mul_self', norm_unitary_smul, of_le_norm_mul_star_self, star_mul_self_eq_zero_iff, star_mul_self_ne_zero_iff, to_normedStarGroup, nnnorm_mul_self, nnnorm_pow_two_pow, norm_mul_self, norm_pow_two_pow, norm_star_le, to_continuousStar, cstarRing, cstarRing', cstarRing, starRingEnd, to_cstarRing, coe_starₗᵢ, instCStarRingReal, nnnorm_star, norm_star, nnnorm_pow_two_pow, star_isometry, starₗᵢ_apply, starₗᵢ_toContinuousLinearEquiv	41
Total	48

CStarRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormOneClassOfNontrivial 📖	mathematical	—	NormOneClass NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing	—	norm_one
mul_star_self_eq_zero_iff 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	star_star star_mul_self_eq_zero_iff
mul_star_self_ne_zero_iff 📖	—	—	—	—	—
nnnorm_self_mul_star 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NNReal NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	norm_self_mul_star
nnnorm_star_mul_self 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid NNReal NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiringNNReal	—	norm_star_mul_self
norm_coe_unitary 📖	mathematical	—	Norm.norm NormedRing.toNorm Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Real Real.instOne	—	sq_eq_sq₀ IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing IsOrderedRing.toMulPosMono Real.instIsOrderedRing norm_nonneg zero_le_one Real.instZeroLEOneClass one_pow sq norm_star_mul_self Unitary.coe_star_mul_self norm_one
norm_coe_unitary_mul 📖	mathematical	—	Norm.norm NormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim norm_of_subsingleton le_antisymm norm_mul_le norm_coe_unitary one_mul Unitary.coe_star_mul_self mul_assoc norm_star to_normedStarGroup
norm_mem_unitary_mul 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	Norm.norm NormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	norm_coe_unitary_mul
norm_mul_coe_unitary 📖	mathematical	—	Norm.norm NormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	—	StarMul.star_mul star_star norm_star to_normedStarGroup norm_mem_unitary_mul Unitary.star_mem Subtype.prop
norm_mul_mem_unitary 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	Norm.norm NormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	norm_mul_coe_unitary
norm_mul_self_le 📖	mathematical	—	Real Real.instLE Real.instMul Norm.norm NonUnitalNormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	—
norm_of_mem_unitary 📖	mathematical	Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	Norm.norm NormedRing.toNorm Real Real.instOne	—	norm_coe_unitary
norm_one 📖	mathematical	—	Norm.norm NormedRing.toNorm AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing Real Real.instOne	—	norm_pos_iff one_ne_zero NeZero.one mul_left_inj' IsCancelMulZero.toIsRightCancelMulZero IsDomain.toIsCancelMulZero Real.instIsDomain LT.lt.ne' norm_star_mul_self mul_one star_one one_mul
norm_self_mul_star 📖	mathematical	—	Norm.norm NonUnitalNormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real Real.instMul	—	star_star norm_star_mul_self norm_star to_normedStarGroup
norm_star_mul_self 📖	mathematical	—	Norm.norm NonUnitalNormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real Real.instMul	—	le_antisymm LE.le.trans norm_mul_le norm_star to_normedStarGroup le_refl norm_mul_self_le
norm_star_mul_self' 📖	mathematical	—	Norm.norm NonUnitalNormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid Real Real.instMul	—	norm_star_mul_self norm_star to_normedStarGroup
norm_unitary_smul 📖	mathematical	—	Norm.norm NormedRing.toNorm Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring NormedRing.toRing SetLike.instMembership Submonoid.instSetLike unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Submonoid.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass ESeminormedAddMonoid.toAddMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup NonUnitalNormedRing.toNormedAddCommGroup NormedRing.toNonUnitalNormedRing ESeminormedAddCommMonoid.toESeminormedAddMonoid ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	norm_coe_unitary_mul
of_le_norm_mul_star_self 📖	mathematical	Real Real.instLE Real.instMul Norm.norm NonUnitalNormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	CStarRing	—	eq_zero_or_norm_pos norm_zero le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing mul_comm star_star LE.le.trans norm_mul_le Function.Surjective.forall Function.Involutive.surjective InvolutiveStar.star_involutive norm_star
star_mul_self_eq_zero_iff 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	norm_eq_zero norm_star_mul_self mul_self_eq_zero NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass
star_mul_self_ne_zero_iff 📖	—	—	—	—	—
to_normedStarGroup 📖	mathematical	—	NormedStarGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing StarRing.toStarAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	eq_zero_or_norm_pos norm_zero le_of_mul_le_mul_right MulPosStrictMono.toMulPosReflectLE IsStrictOrderedRing.toMulPosStrictMono Real.instIsStrictOrderedRing star_star LE.le.trans norm_mul_self_le norm_mul_le

CStarRing.MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instMulOpposite 📖	mathematical	—	CStarRing MulOpposite MulOpposite.instNonUnitalNormedRing MulOpposite.instStarRing NonUnitalRing.toNonUnitalSemiring NonUnitalNormedRing.toNonUnitalRing	—	Eq.le CStarRing.norm_self_mul_star

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_mul_self 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing StarRing.toStarAddMonoid	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NNReal Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero instSemiringNNReal	—	norm_mul_self
nnnorm_pow_two_pow 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing StarRing.toStarAddMonoid	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Nat.instMonoid NNReal instSemiringNNReal	—	pow_zero pow_one pow_succ' pow_mul' sq nnnorm_mul_self pow
norm_mul_self 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing StarRing.toStarAddMonoid	Norm.norm NonUnitalNormedRing.toNorm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Real Monoid.toNatPow Real.instMonoid	—	sq star_eq CStarRing.norm_star_mul_self
norm_pow_two_pow 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing StarRing.toStarAddMonoid	Norm.norm NormedRing.toNorm Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Nat.instMonoid Real Real.instMonoid	—	nnnorm_pow_two_pow

NormedStarGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
norm_star_le 📖	mathematical	—	Real Real.instLE Norm.norm SeminormedAddCommGroup.toNorm Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	—
to_continuousStar 📖	mathematical	—	ContinuousStar UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	Isometry.continuous star_isometry

Pi

Definitions

Name	Category	Theorems
starRing' 📖	CompOp	5 math math: MeasureTheory.lpNorm_conj, cstarRing', AnalyticAt.harmonicAt_conj, cstarRing, MeasureTheory.eLpNorm_conj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cstarRing 📖	mathematical	CStarRing	nonUnitalNormedRing starRing'	—	le_of_eq CStarRing.nnnorm_star_mul_self Finset.comp_sup_eq_sup_comp_of_is_total sq mul_le_mul' NNReal.mulLeftMono covariant_swap_mul_of_covariant_mul bot_eq_zero' NNReal.instCanonicallyOrderedAdd zero_pow Nat.instCharZero Nat.instAtLeastTwoHAddOfNat
cstarRing' 📖	mathematical	—	CStarRing nonUnitalNormedRing starRing'	—	cstarRing

Prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cstarRing 📖	mathematical	—	CStarRing nonUnitalNormedRing instStarRing NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalRing.toNonUnitalNonAssocRing NonUnitalNormedRing.toNonUnitalRing	—	CStarRing.norm_star_mul_self le_sup_iff le_total sup_of_le_right sup_of_le_left

RingHomIsometric

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
starRingEnd 📖	mathematical	—	RingHomIsometric CommSemiring.toSemiring CommRing.toCommSemiring NormedCommRing.toCommRing NormedRing.toNorm NormedCommRing.toNormedRing starRingEnd	—	norm_star

StarSubalgebra

Definitions

Name	Category	Theorems
toNormedAlgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_cstarRing 📖	mathematical	—	CStarRing StarSubalgebra CommRing.toCommSemiring Ring.toSemiring NormedRing.toRing SetLike.instMembership setLike NormedRing.toNonUnitalNormedRing SubringClass.toNormedRing subringClass starRing	—	subringClass CStarRing.norm_mul_self_le

(root)

Definitions

Name	Category	Theorems
CStarRing 📖	CompData	21 math math: NonUnitalCStarAlgebra.toCStarRing, CommCStarAlgebra.toCStarRing, Quaternion.instCStarRingReal, RCLike.instCStarRing, Prod.cstarRing, ContinuousLinearMap.instCStarRingId, Pi.cstarRing', CStarRing.MulOpposite.instMulOpposite, instCStarRingReal, ContinuousMap.instCStarRing, DoubleCentralizer.instCStarRing, BoundedContinuousFunction.instCStarRing, ZeroAtInftyContinuousMap.instCStarRing, NonUnitalCommCStarAlgebra.toCStarRing, CStarAlgebra.toCStarRing, Unitization.instCStarRing, StarSubalgebra.to_cstarRing, ContinuousMapZero.instCStarRing, Matrix.instCStarRing, CStarMatrix.instCStarRing, CStarRing.of_le_norm_mul_star_self
NormedStarGroup 📖	CompData	6 math math: ZeroAtInftyContinuousMap.instNormedStarGroup, Matrix.frobenius_normedStarGroup, ContinuousMap.instNormedStarGroup, BoundedContinuousFunction.instNormedStarGroup, CStarRing.to_normedStarGroup, Matrix.instNormedStarGroup
instNormedSpaceSubtypeMemAddSubgroupSelfAdjointOfTrivialStarOfStarModule 📖	CompOp	—
starNormedAddGroupHom 📖	CompOp	—
starₗᵢ 📖	CompOp	3 math math: starₗᵢ_apply, starₗᵢ_toContinuousLinearEquiv, coe_starₗᵢ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_starₗᵢ 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd EquivLike.toFunLike LinearIsometryEquiv.instEquivLike starₗᵢ Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	RingHomInvPair.instStarRingEnd
instCStarRingReal 📖	mathematical	—	CStarRing Real NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Real.normedCommRing instStarRingReal	—	abs_mul_abs_self norm_mul NormedDivisionRing.toNormMulClass
nnnorm_star 📖	mathematical	—	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup	—	norm_star
norm_star 📖	mathematical	—	Norm.norm SeminormedAddCommGroup.toNorm Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	le_antisymm NormedStarGroup.norm_star_le star_star
star_isometry 📖	mathematical	—	Isometry PseudoMetricSpace.toPseudoEMetricSpace SeminormedAddCommGroup.toPseudoMetricSpace Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	AddMonoidHomClass.isometry_of_norm AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass norm_star
starₗᵢ_apply 📖	mathematical	—	DFunLike.coe LinearIsometryEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd EquivLike.toFunLike LinearIsometryEquiv.instEquivLike starₗᵢ Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SeminormedAddGroup.toAddGroup SeminormedAddCommGroup.toSeminormedAddGroup	—	RingHomInvPair.instStarRingEnd
starₗᵢ_toContinuousLinearEquiv 📖	mathematical	—	LinearIsometryEquiv.toContinuousLinearEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd starₗᵢ starL AddCommGroup.toAddCommMonoid SeminormedAddCommGroup.toAddCommGroup UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedStarGroup.to_continuousStar	—	ContinuousLinearEquiv.ext RingHomInvPair.instStarRingEnd NormedStarGroup.to_continuousStar

selfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nnnorm_pow_two_pow 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NormedRing.toRing StarRing.toStarAddMonoid	NNNorm.nnnorm SeminormedAddGroup.toNNNorm SeminormedAddCommGroup.toSeminormedAddGroup NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalNormedRing.toNonUnitalSeminormedRing NormedRing.toNonUnitalNormedRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Nat.instMonoid NNReal instSemiringNNReal	—	IsSelfAdjoint.nnnorm_pow_two_pow

---

← Back to Index