LinearMap

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

Statistics

Metric	Count
Definitions convIntrinsicStarRing, intrinsicInvolutiveStar, intrinsicStar, intrinsicStarAddMonoid, intrinsicStar, convIntrinsicStarRingCommSemiring	6
Theorems isSelfAdjoint, isSelfAdjoint_iff_map_star, isSelfAdjoint_iff_toMatrix', starLinearEquiv_eq_arrowCongr, intrinsicStarModule, intrinsicStar_apply, intrinsicStar_comp, intrinsicStar_comp', intrinsicStar_convMul, intrinsicStar_eq_comp, intrinsicStar_id, intrinsicStar_lTensor, intrinsicStar_mul', intrinsicStar_mulLeft, intrinsicStar_mulRight, intrinsicStar_rTensor, intrinsicStar_single, intrinsicStar_smulRight, intrinsicStar_toSpanSingleton, intrinsicStar_zero, isSelfAdjoint_iff_map_star, toMatrix'_intrinsicStar, isSelfAdjoint_toLin'_iff, intrinsicStar_toLin', intrinsicStar, isUnit_intrinsicStar_iff, mem_eigenspace_intrinsicStar_iff, spectrum_intrinsicStar, intrinsicStar_comul, intrinsicStar_comul_commSemiring, isSelfAdjoint, intrinsicStar_map, star_map_apply_eq_map_intrinsicStar	33
Total	39

IntrinsicStar.StarHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint 📖	mathematical	—	IsSelfAdjoint WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.intrinsicStar WithConv.toConv SemilinearMapClass.semilinearMap	—	LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star StarHomClass.map_star

LinearMap

Definitions

Name	Category	Theorems
convIntrinsicStarRing 📖	CompOp	—
intrinsicInvolutiveStar 📖	CompOp	—
intrinsicStar 📖	CompOp	30 math math: intrinsicStar_mulRight, Module.End.spectrum_intrinsicStar, Matrix.intrinsicStar_toLin', intrinsicStar_toSpanSingleton, Module.End.mem_eigenspace_intrinsicStar_iff, Pi.intrinsicStar_comul_commSemiring, intrinsicStar_mul', intrinsicStar_zero, IntrinsicStar.isSelfAdjoint_iff_map_star, intrinsicStar_comp', intrinsicStar_rTensor, TensorProduct.intrinsicStar_map, Matrix.IntrinsicStar.isSelfAdjoint_toLin'_iff, toMatrix'_intrinsicStar, intrinsicStar_id, intrinsicStar_mulLeft, intrinsicStar_lTensor, intrinsicStarModule, intrinsicStar_single, intrinsicStar_smulRight, IntrinsicStar.isSelfAdjoint_iff_toMatrix', intrinsicStar_apply, isSelfAdjoint_iff_map_star, IntrinsicStar.StarHomClass.isSelfAdjoint, Module.End.isUnit_intrinsicStar_iff, StarHomClass.isSelfAdjoint, intrinsicStar_comp, TensorProduct.star_map_apply_eq_map_intrinsicStar, Module.End.IsUnit.intrinsicStar, intrinsicStar_eq_comp
intrinsicStarAddMonoid 📖	CompOp	1 math math: IntrinsicStar.starLinearEquiv_eq_arrowCongr

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intrinsicStarModule 📖	mathematical	—	StarModule WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring InvolutiveStar.toStar intrinsicStar SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass WithConv.instAddMonoid AddCommMonoid.toAddMonoid addCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero WithConv.instDistribMulAction instDistribMulAction Module.toDistribMulAction	—	WithConv.ext ext StarModule.star_smul
intrinsicStar_apply 📖	mathematical	—	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike WithConv.ofConv Star.star WithConv intrinsicStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	—
intrinsicStar_comp 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring intrinsicStar WithConv.toConv comp RingHomCompTriple.ids WithConv.ofConv	—	WithConv.ext RingHomCompTriple.ids ext star_star
intrinsicStar_comp' 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring intrinsicStar WithConv.toConv comp RingHomCompTriple.ids WithConv.ofConv	—	intrinsicStar_comp
intrinsicStar_convMul 📖	mathematical	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid TensorProduct.instStarAddMonoid TensorProduct.instStarModule WithConv.toConv CoalgebraStruct.comul comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.comm	convMul	—	TensorProduct.instStarModule RingHomCompTriple.ids RingHomInvPair.ids intrinsicStar_comp' comp.congr_simp intrinsicStar_mul' TensorProduct.intrinsicStar_map comp_assoc RingHomCompTriple.right_ids TensorProduct.map_comp_comm_eq WithConv.ext ext TensorProduct.comm_comm
intrinsicStar_eq_comp 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid WithConv.toConv comp starRingEnd RingHomInvPair.triples₂ RingHomInvPair.instStarRingEnd LinearEquiv.toLinearMap starLinearEquiv RingHomCompTriple.right_ids WithConv.ofConv	—	—
intrinsicStar_id 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring intrinsicStar WithConv.toConv id	—	WithConv.ext ext star_star
intrinsicStar_lTensor 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid TensorProduct.instStarAddMonoid TensorProduct.instStarModule WithConv.toConv lTensor WithConv.ofConv	—	WithConv.ext TensorProduct.instStarModule TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower ext IsScalarTower.to_smulCommClass star_star
intrinsicStar_mul' 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid TensorProduct.addCommMonoid TensorProduct.instModule intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid TensorProduct.instStarAddMonoid TensorProduct.instStarModule WithConv.toConv mul' comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.comm	—	WithConv.ext TensorProduct.instStarModule RingHomCompTriple.ids RingHomInvPair.ids TensorProduct.ext' StarMul.star_mul star_star
intrinsicStar_mulLeft 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid intrinsicStar StarRing.toStarAddMonoid WithConv.toConv mulLeft mulRight InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	WithConv.ext ext StarMul.star_mul star_star
intrinsicStar_mulRight 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid intrinsicStar StarRing.toStarAddMonoid WithConv.toConv mulRight mulLeft InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	star_eq_iff_star_eq intrinsicStar_mulLeft star_star
intrinsicStar_rTensor 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid TensorProduct.instStarAddMonoid TensorProduct.instStarModule WithConv.toConv rTensor WithConv.ofConv	—	WithConv.ext TensorProduct.instStarModule TensorProduct.AlgebraTensorModule.curry_injective IsScalarTower.left TensorProduct.isScalarTower ext IsScalarTower.to_smulCommClass star_star
intrinsicStar_single 📖	mathematical	StarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	Star.star WithConv LinearMap RingHom.id Pi.addCommMonoid Pi.module intrinsicStar Pi.instStarAddMonoidForall Pi.instStarModuleForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction WithConv.toConv single	—	WithConv.ext Pi.instStarModuleForall ext star_zero star_star
intrinsicStar_smulRight 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring intrinsicStar StarAddMonoid.toInvolutiveStar AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne WithConv.toConv smulRight Semiring.toModule IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction WithConv.ofConv NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring InvolutiveStar.toStar	—	WithConv.ext IsScalarTower.left ext StarModule.star_smul
intrinsicStar_toSpanSingleton 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule intrinsicStar StarAddMonoid.toInvolutiveStar AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne WithConv.toConv toSpanSingleton InvolutiveStar.toStar AddCommMonoid.toAddMonoid	—	WithConv.ext ext_ring StarModule.star_smul star_star one_smul
intrinsicStar_zero 📖	mathematical	—	Star.star WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring intrinsicStar AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass WithConv.instAddMonoid AddCommMonoid.toAddMonoid addCommMonoid	—	star_zero
isSelfAdjoint_iff_map_star 📖	mathematical	—	IsSelfAdjoint WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring intrinsicStar DFunLike.coe instFunLike WithConv.ofConv Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	IntrinsicStar.isSelfAdjoint_iff_map_star
toMatrix'_intrinsicStar 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule Matrix addCommMonoid Matrix.addCommMonoid module Function.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toMatrix' WithConv.ofConv Star.star WithConv intrinsicStar StarAddMonoid.toInvolutiveStar StarRing.toStarAddMonoid Pi.instStarAddMonoidForall Pi.instStarModuleForall InvolutiveStar.toStar StarMul.toStarModule CommSemiring.toCommMonoid StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Matrix.map	—	Matrix.ext RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Pi.instStarModuleForall StarMul.toStarModule Pi.star_single star_one

LinearMap.IntrinsicStar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint_iff_map_star 📖	mathematical	—	IsSelfAdjoint WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.intrinsicStar DFunLike.coe LinearMap.instFunLike WithConv.ofConv Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid	—	—
isSelfAdjoint_iff_toMatrix' 📖	mathematical	—	IsSelfAdjoint WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instStarAddMonoidForall Pi.instStarModuleForall SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction InvolutiveStar.toStar StarMul.toStarModule CommSemiring.toCommMonoid StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module Function.smulCommClass DistribMulAction.toMulAction Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix' WithConv.ofConv	—	Pi.instStarModuleForall StarMul.toStarModule RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass LinearEquiv.injective LinearMap.toMatrix'_intrinsicStar
starLinearEquiv_eq_arrowCongr 📖	mathematical	—	starLinearEquiv WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring WithConv.instAddCommMonoid LinearMap.addCommMonoid LinearMap.intrinsicStarAddMonoid StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid WithConv.instModule LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Module.toDistribMulAction LinearMap.intrinsicStarModule LinearEquiv.trans starRingEnd RingHomCompTriple.ids RingHomCompTriple.right_ids RingHomInvPair.ids RingHomInvPair.instStarRingEnd WithConv.linearEquiv LinearEquiv.arrowCongr RingHomInvPair.triples₂ LinearEquiv.symm	—	RingHomInvPair.instStarRingEnd smulCommClass_self LinearMap.intrinsicStarModule

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intrinsicStar_toLin' 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instStarAddMonoidForall Pi.instStarModuleForall SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction InvolutiveStar.toStar StarMul.toStarModule CommSemiring.toCommMonoid StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring WithConv.toConv DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module Function.smulCommClass DistribMulAction.toMulAction Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLin' map	—	Pi.instStarModuleForall StarMul.toStarModule RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass LinearEquiv.injective LinearMap.toMatrix'_intrinsicStar LinearMap.toMatrix'_toLin'

Matrix.IntrinsicStar

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint_toLin'_iff 📖	mathematical	—	IsSelfAdjoint WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Pi.Function.module Semiring.toModule LinearMap.intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid Pi.instStarAddMonoidForall Pi.instStarModuleForall SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction InvolutiveStar.toStar StarMul.toStarModule CommSemiring.toCommMonoid StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring WithConv.toConv DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix Matrix.addCommMonoid LinearMap.addCommMonoid Matrix.module LinearMap.module Function.smulCommClass DistribMulAction.toMulAction Module.toDistribMulAction Algebra.to_smulCommClass Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Matrix.toLin'	—	Pi.instStarModuleForall StarMul.toStarModule RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Matrix.intrinsicStar_toLin' EquivLike.toEmbeddingLike

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isUnit_intrinsicStar_iff 📖	mathematical	—	IsUnit Module.End instMonoid WithConv.ofConv Star.star WithConv LinearMap.intrinsicStar	—	IsUnit.intrinsicStar star_star
mem_eigenspace_intrinsicStar_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike eigenspace WithConv.ofConv Module.End Star.star WithConv LinearMap.intrinsicStar InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	StarModule.star_smul
spectrum_intrinsicStar 📖	mathematical	—	spectrum Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instRing instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero WithConv.ofConv Star.star WithConv LinearMap.intrinsicStar Set InvolutiveStar.toStar Set.instInvolutiveStar	—	Set.ext smulCommClass_self IsScalarTower.left Algebra.algebraMap_eq_smul_one isUnit_intrinsicStar_iff star_sub StarModule.star_smul LinearMap.intrinsicStarModule LinearMap.intrinsicStar_id star_star

Module.End.IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intrinsicStar 📖	mathematical	IsUnit Module.End Module.End.instMonoid WithConv.ofConv	Star.star WithConv LinearMap.intrinsicStar	—	Units.isUnit

Module.End.Units

Definitions

Name	Category	Theorems
intrinsicStar 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
convIntrinsicStarRingCommSemiring 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intrinsicStar_comul 📖	mathematical	StarModule InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring StarRing.toStarAddMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Star.star WithConv LinearMap RingHom.id TensorProduct TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.intrinsicStar TensorProduct.instStarAddMonoid TensorProduct.instStarModule WithConv.toConv CoalgebraStruct.comul LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids TensorProduct.comm	addCommMonoid module instStarAddMonoidForall instStarModuleForall SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction instCoalgebraStruct	—	TensorProduct.instStarModule RingHomCompTriple.ids RingHomInvPair.ids WithConv.ext instStarModuleForall LinearMap.pi_ext' Finite.of_fintype LinearMap.ext star_single comul_single TensorProduct.star_map_apply_eq_map_intrinsicStar TensorProduct.map_comm LinearMap.intrinsicStar_single
intrinsicStar_comul_commSemiring 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring module Semiring.toModule TensorProduct.addCommMonoid TensorProduct.instModule LinearMap.intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid StarRing.toStarAddMonoid instStarAddMonoidForall instStarModuleForall SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction InvolutiveStar.toStar StarMul.toStarModule CommSemiring.toCommMonoid StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring TensorProduct.instStarAddMonoid TensorProduct.instStarModule WithConv.toConv CoalgebraStruct.comul instCoalgebraStruct Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra LinearMap.comp RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids Function.module TensorProduct.comm	—	intrinsicStar_comul StarMul.toStarModule WithConv.ext TensorProduct.instStarModule RingHomCompTriple.ids RingHomInvPair.ids LinearMap.ext_ring star_one Coalgebra.comm_comp_comul CommSemiring.instIsCocomm

StarHomClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isSelfAdjoint 📖	mathematical	—	IsSelfAdjoint WithConv LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.intrinsicStar WithConv.toConv SemilinearMapClass.semilinearMap	—	IntrinsicStar.StarHomClass.isSelfAdjoint

TensorProduct

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intrinsicStar_map 📖	mathematical	—	Star.star WithConv LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring TensorProduct addCommMonoid instModule LinearMap.intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid instStarAddMonoid instStarModule WithConv.toConv map WithConv.ofConv	—	WithConv.ext instStarModule ext'
star_map_apply_eq_map_intrinsicStar 📖	mathematical	—	Star.star TensorProduct instStar DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring addCommMonoid instModule LinearMap.instFunLike map WithConv.ofConv WithConv LinearMap.intrinsicStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring StarRing.toStarAddMonoid	—	instStarModule star_star intrinsicStar_map

---

← Back to Index