Prod

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

Statistics

Metric	Count
Definitions instInvolutiveStar, instStarAddMonoid, instStarMul, instStarRing	4
Theorems instStarModule, instTrivialStar, embed_product_star	3
Total	7

Prod

Definitions

Name	Category	Theorems
instInvolutiveStar 📖	CompOp	—
instStarAddMonoid 📖	CompOp	—
instStarMul 📖	CompOp	—
instStarRing 📖	CompOp	11 math math: instStarOrderedRing, cstarRing, cfc_map_prod, CFC.sqrt_map_prod, CFC.rpow_map_prod, cfcₙ_map_prod, NonUnitalStarSubalgebra.prod_inf_prod, CFC.nnrpow_eq_nnrpow_prod, NonUnitalStarSubalgebra.prod_top, CFC.rpow_eq_rpow_prod, CFC.nnrpow_map_prod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instStarModule 📖	mathematical	—	StarModule instStar instSMul	—	StarModule.star_smul
instTrivialStar 📖	mathematical	—	TrivialStar instStar	—	TrivialStar.star_trivial

Units

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embed_product_star 📖	mathematical	—	DFunLike.coe MonoidHom Units MulOpposite MulOneClass.toMulOne instMulOneClass Prod.instMulOneClass Monoid.toMulOneClass MulOpposite.instMulOneClass MonoidHom.instFunLike embedProduct Star.star InvolutiveStar.toStar StarMul.toInvolutiveStar instMul instStarMul Prod.instStar MulOne.toMul MulOpposite.instStar	—	—

---

← Back to Index