Star

📁 Source: Mathlib/Topology/Algebra/Module/Star.lean

Statistics

Metric	Count
Definitions decomposeProdAdjointL, selfAdjointPartL, skewAdjointPartL, starL, starL', «term_→L⋆[_]_», «term_≃L⋆[_]_»	7
Theorems decomposeProdAdjointL_apply, decomposeProdAdjointL_symm_apply, continuous_decomposeProdAdjoint, continuous_decomposeProdAdjoint_symm, continuous_selfAdjointPart, continuous_skewAdjointPart, selfAdjointPartL_apply_coe, skewAdjointPartL_apply_coe, starL'_apply, starL'_symm_apply, starL_apply, starL_symm_apply	12
Total	19

StarModule

Definitions

Name	Category	Theorems
decomposeProdAdjointL 📖	CompOp	2 math math: decomposeProdAdjointL_symm_apply, decomposeProdAdjointL_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decomposeProdAdjointL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint skewAdjoint instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid AddSubgroup.toAddCommGroup Prod.instModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike decomposeProdAdjointL LinearMap LinearMap.instFunLike selfAdjointPart skewAdjointPart	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids
decomposeProdAdjointL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint skewAdjoint instTopologicalSpaceProd instTopologicalSpaceSubtype Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Prod.instModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm decomposeProdAdjointL AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap LinearMap.instFunLike Submodule.subtype selfAdjoint.submodule skewAdjoint.submodule	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids

(root)

Definitions

Name	Category	Theorems
selfAdjointPartL 📖	CompOp	1 math math: selfAdjointPartL_apply_coe
skewAdjointPartL 📖	CompOp	1 math math: skewAdjointPartL_apply_coe
starL 📖	CompOp	4 math math: starL_apply, starL_symm_apply, starₗᵢ_toContinuousLinearEquiv, HasFDerivAt.star_star
starL' 📖	CompOp	8 math math: HasStrictFDerivAt.star, HasFDerivAt.star, fderivWithin_star, HasFDerivWithinAt.star, starL'_apply, HasFDerivAtFilter.star, starL'_symm_apply, fderiv_star
«term_→L⋆[_]_» 📖	CompOp	—
«term_≃L⋆[_]_» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
continuous_decomposeProdAdjoint 📖	mathematical	—	Continuous AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint skewAdjoint instTopologicalSpaceProd instTopologicalSpaceSubtype DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddCommGroup.toAddCommMonoid Prod.instAddCommMonoid AddSubgroup.toAddCommGroup Prod.instModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule EquivLike.toFunLike LinearEquiv.instEquivLike StarModule.decomposeProdAdjoint	—	Nat.instAtLeastTwoHAddOfNat Continuous.prodMk continuous_selfAdjointPart IsTopologicalAddGroup.toContinuousAdd continuous_skewAdjointPart IsTopologicalAddGroup.to_continuousSub
continuous_decomposeProdAdjoint_symm 📖	mathematical	—	Continuous AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint skewAdjoint instTopologicalSpaceProd instTopologicalSpaceSubtype DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Prod.instAddCommMonoid AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup Prod.instModule selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm StarModule.decomposeProdAdjoint	—	Nat.instAtLeastTwoHAddOfNat Continuous.add Continuous.comp continuous_subtype_val continuous_fst continuous_snd
continuous_selfAdjointPart 📖	mathematical	—	Continuous AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint instTopologicalSpaceSubtype DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike selfAdjointPart	—	Nat.instAtLeastTwoHAddOfNat Continuous.comp ContinuousConstSMul.continuous_const_smul Continuous.add continuous_id ContinuousStar.continuous_star
continuous_skewAdjointPart 📖	mathematical	—	Continuous AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint instTopologicalSpaceSubtype DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike skewAdjointPart	—	Nat.instAtLeastTwoHAddOfNat Continuous.comp ContinuousConstSMul.continuous_const_smul Continuous.sub continuous_id ContinuousStar.continuous_star
selfAdjointPartL_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instTopologicalSpaceSubtype AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring ContinuousLinearMap.funLike selfAdjointPartL AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SMulZeroClass.toSMul AddZero.toZero DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Invertible.invOf AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast Star.star StarAddMonoid.toInvolutiveStar	—	Nat.instAtLeastTwoHAddOfNat smul_add
skewAdjointPartL_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint DFunLike.coe ContinuousLinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instTopologicalSpaceSubtype AddSubgroup.toAddCommGroup skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring ContinuousLinearMap.funLike skewAdjointPartL SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Invertible.invOf AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instOfNatAtLeastTwo AddMonoidWithOne.toNatCast SubNegMonoid.toSub Star.star StarAddMonoid.toInvolutiveStar	—	Nat.instAtLeastTwoHAddOfNat
starL'_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike starL' Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	RingHomInvPair.ids
starL'_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm starL' AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddEquiv.instEquivLike AddEquiv.symm starAddEquiv LinearEquiv starRingEnd RingHomInvPair.instStarRingEnd LinearEquiv.instEquivLike LinearEquiv.symm AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	RingHomInvPair.ids
starL_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd EquivLike.toFunLike ContinuousLinearEquiv.equivLike starL Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	RingHomInvPair.instStarRingEnd
starL_symm_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd EquivLike.toFunLike ContinuousLinearEquiv.equivLike ContinuousLinearEquiv.symm starL AddEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid AddEquiv.instEquivLike AddEquiv.symm starAddEquiv	—	RingHomInvPair.instStarRingEnd

---

← Back to Index