Module

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

Statistics

Metric	Count
Definitions decomposeProdAdjoint, submodule, selfAdjointPart, submodule, skewAdjointPart, starLinearEquiv	6
Theorems star_iff, algebraMap, coe_selfAdjointPart_apply, selfAdjointPart_apply, skewAdjointPart_apply, toStarModuleNNRat, toStarModuleRat, decomposeProdAdjoint_apply, decomposeProdAdjoint_symm_apply, selfAdjointPart_add_skewAdjointPart, algebraMap_star_comm, isSelfAdjoint_algebraMap_iff, selfAdjointPart_apply_coe, selfAdjointPart_comp_subtype_selfAdjoint, selfAdjointPart_comp_subtype_skewAdjoint, skewAdjointPart_apply_coe, skewAdjointPart_comp_subtype_selfAdjoint, skewAdjointPart_comp_subtype_skewAdjoint, starLinearEquiv_apply, starLinearEquiv_symm_apply, star_intCast_smul, star_inv_intCast_smul, star_inv_natCast_smul, star_natCast_smul, star_nnqsmul, star_nnrat_smul, star_qsmul, star_ratCast_smul, star_rat_smul	29
Total	35

IsIdempotentElem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
star_iff 📖	mathematical	—	IsIdempotentElem Star.star InvolutiveStar.toStar StarMul.toInvolutiveStar	—	—

IsSelfAdjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid	StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	algebraMap_star_comm star_eq
coe_selfAdjointPart_apply 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike selfAdjointPart	—	Nat.instAtLeastTwoHAddOfNat selfAdjointPart_apply_coe star_eq smul_add invOf_two_smul_add_invOf_two_smul
selfAdjointPart_apply 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddSubgroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike selfAdjointPart	—	Nat.instAtLeastTwoHAddOfNat coe_selfAdjointPart_apply
skewAdjointPart_apply 📖	mathematical	IsSelfAdjoint InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddSubgroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint AddCommGroup.toAddCommMonoid AddSubgroup.toAddCommGroup skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike skewAdjointPart AddSubgroup.zero	—	Nat.instAtLeastTwoHAddOfNat skewAdjointPart_apply_coe star_eq sub_self smul_zero AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass AddSubgroup.instAddSubgroupClass ZeroMemClass.coe_zero

StarAddMonoid

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toStarModuleNNRat 📖	mathematical	—	StarModule NNRat InvolutiveStar.toStar toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield StarRing.toStarAddMonoid NNRat.instStarRing SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	star_nnrat_smul
toStarModuleRat 📖	mathematical	—	StarModule InvolutiveStar.toStar toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Rat.commRing StarRing.toStarAddMonoid Rat.instStarRing SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring AddCommGroup.toAddCommMonoid	—	star_rat_smul

StarModule

Definitions

Name	Category	Theorems
decomposeProdAdjoint 📖	CompOp	4 math math: continuous_decomposeProdAdjoint, continuous_decomposeProdAdjoint_symm, decomposeProdAdjoint_symm_apply, decomposeProdAdjoint_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
decomposeProdAdjoint_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint skewAdjoint 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 decomposeProdAdjoint LinearMap LinearMap.instFunLike selfAdjointPart skewAdjointPart	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids
decomposeProdAdjoint_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint skewAdjoint 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 decomposeProdAdjoint AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup LinearMap LinearMap.instFunLike Submodule.subtype selfAdjoint.submodule skewAdjoint.submodule	—	Nat.instAtLeastTwoHAddOfNat RingHomInvPair.ids
selfAdjointPart_add_skewAdjointPart 📖	mathematical	—	AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AddSubgroup.toAddCommGroup selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.instFunLike selfAdjointPart skewAdjoint skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule skewAdjointPart	—	Nat.instAtLeastTwoHAddOfNat smul_add smul_sub add_add_sub_cancel invOf_two_smul_add_invOf_two_smul

(root)

Definitions

Name	Category	Theorems
selfAdjointPart 📖	CompOp	9 math math: StarModule.selfAdjointPart_add_skewAdjointPart, selfAdjointPart_comp_subtype_skewAdjoint, IsSelfAdjoint.selfAdjointPart_apply, StarModule.decomposeProdAdjointL_apply, selfAdjointPart_comp_subtype_selfAdjoint, continuous_selfAdjointPart, IsSelfAdjoint.coe_selfAdjointPart_apply, selfAdjointPart_apply_coe, StarModule.decomposeProdAdjoint_apply
skewAdjointPart 📖	CompOp	10 math math: StarModule.selfAdjointPart_add_skewAdjointPart, StarModule.decomposeProdAdjointL_apply, IsSelfAdjoint.skewAdjointPart_apply, imaginaryPart_eq_neg_I_smul_skewAdjointPart, skewAdjointPart_comp_subtype_selfAdjoint, skewAdjointPart_apply_coe, skewAdjointPart_eq_I_smul_imaginaryPart, skewAdjointPart_comp_subtype_skewAdjoint, continuous_skewAdjointPart, StarModule.decomposeProdAdjoint_apply
starLinearEquiv 📖	CompOp	5 math math: starLinearEquiv_symm_apply, LinearMap.IntrinsicStar.starLinearEquiv_eq_arrowCongr, starLinearEquiv_tensor, starLinearEquiv_apply, LinearMap.intrinsicStar_eq_comp

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_star_comm 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	Algebra.algebraMap_eq_smul_one StarModule.star_smul star_one
isSelfAdjoint_algebraMap_iff 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	IsSelfAdjoint InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid	—	IsSelfAdjoint.star_eq algebraMap_star_comm IsSelfAdjoint.algebraMap
selfAdjointPart_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike selfAdjoint 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 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 AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup Star.star StarAddMonoid.toInvolutiveStar	—	Nat.instAtLeastTwoHAddOfNat
selfAdjointPart_comp_subtype_selfAdjoint 📖	mathematical	—	LinearMap.comp Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike selfAdjoint.submodule AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike selfAdjoint Submodule.addCommMonoid AddSubgroup.toAddCommGroup Submodule.module selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id RingHomCompTriple.ids selfAdjointPart Submodule.subtype LinearMap.id	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext RingHomCompTriple.ids IsSelfAdjoint.selfAdjointPart_apply
selfAdjointPart_comp_subtype_skewAdjoint 📖	mathematical	—	LinearMap.comp Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike skewAdjoint.submodule AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike selfAdjoint Submodule.addCommMonoid AddSubgroup.toAddCommGroup Submodule.module selfAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id RingHomCompTriple.ids selfAdjointPart Submodule.subtype LinearMap LinearMap.instZero	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext RingHomCompTriple.ids add_neg_cancel smul_zero
skewAdjointPart_apply_coe 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership AddSubgroup.instSetLike skewAdjoint 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 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
skewAdjointPart_comp_subtype_selfAdjoint 📖	mathematical	—	LinearMap.comp Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike selfAdjoint.submodule AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike skewAdjoint Submodule.addCommMonoid AddSubgroup.toAddCommGroup Submodule.module skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id RingHomCompTriple.ids skewAdjointPart Submodule.subtype LinearMap LinearMap.instZero	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext RingHomCompTriple.ids IsSelfAdjoint.skewAdjointPart_apply
skewAdjointPart_comp_subtype_skewAdjoint 📖	mathematical	—	LinearMap.comp Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike skewAdjoint.submodule AddSubgroup AddCommGroup.toAddGroup AddSubgroup.instSetLike skewAdjoint Submodule.addCommMonoid AddSubgroup.toAddCommGroup Submodule.module skewAdjoint.instModuleSubtypeMemAddSubgroupOfStarModule InvolutiveStar.toStar StarMul.toInvolutiveStar Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring RingHom.id RingHomCompTriple.ids skewAdjointPart Submodule.subtype LinearMap.id	—	Nat.instAtLeastTwoHAddOfNat LinearMap.ext RingHomCompTriple.ids sub_neg_eq_add smul_add invOf_two_smul_add_invOf_two_smul
starLinearEquiv_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd EquivLike.toFunLike LinearEquiv.instEquivLike starLinearEquiv Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	RingHomInvPair.instStarRingEnd
starLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring starRingEnd RingHomInvPair.instStarRingEnd EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm starLinearEquiv Equiv.invFun AddEquiv.toEquiv AddSemigroup.toAdd AddMonoid.toAddSemigroup AddCommMonoid.toAddMonoid starAddEquiv	—	RingHomInvPair.instStarRingEnd
star_intCast_smul 📖	mathematical	—	Star.star 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 AddGroupWithOne.toIntCast Ring.toAddGroupWithOne	—	map_intCast_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
star_inv_intCast_smul 📖	mathematical	—	Star.star 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 DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddGroupWithOne.toIntCast Ring.toAddGroupWithOne DivisionRing.toRing	—	map_inv_intCast_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
star_inv_natCast_smul 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	map_inv_natCast_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
star_natCast_smul 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	map_natCast_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
star_nnqsmul 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction	—	star_nnrat_smul
star_nnrat_smul 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NNRat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring NNRat.instSemifield Module.toDistribMulAction	—	map_nnrat_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
star_qsmul 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring AddCommGroup.toAddCommMonoid	—	star_rat_smul
star_ratCast_smul 📖	mathematical	—	Star.star 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 DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid DivisionRing.toRatCast	—	map_ratCast_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass
star_rat_smul 📖	mathematical	—	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Rat.monoid Module.toDistribMulAction Rat.semiring AddCommGroup.toAddCommMonoid	—	map_rat_smul AddEquivClass.instAddMonoidHomClass AddEquiv.instAddEquivClass

selfAdjoint

Definitions

Name	Category	Theorems
submodule 📖	CompOp	6 math math: StarModule.decomposeProdAdjointL_symm_apply, selfAdjointPart_comp_subtype_selfAdjoint, StarModule.decomposeProdAdjoint_symm_apply, realPart_comp_subtype_selfAdjoint, skewAdjointPart_comp_subtype_selfAdjoint, imaginaryPart_comp_subtype_selfAdjoint

skewAdjoint

Definitions

Name	Category	Theorems
submodule 📖	CompOp	4 math math: StarModule.decomposeProdAdjointL_symm_apply, selfAdjointPart_comp_subtype_skewAdjoint, StarModule.decomposeProdAdjoint_symm_apply, skewAdjointPart_comp_subtype_skewAdjoint

---

← Back to Index