Free

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

Statistics

Metric	Count
Definitions instStarRing, starHom, instStarMul	3
Theorems star_algebraMap, star_ι, star_of, star_one	4
Total	7

FreeAlgebra

Definitions

Name	Category	Theorems
instStarRing 📖	CompOp	2 math math: star_algebraMap, star_ι
starHom 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
star_algebraMap 📖	mathematical	—	Star.star FreeAlgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring StarRing.toStarAddMonoid instStarRing DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap instAlgebra Algebra.id	—	AlgHom.commutes
star_ι 📖	mathematical	—	Star.star FreeAlgebra InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSemiring StarRing.toStarAddMonoid instStarRing ι	—	lift_ι_apply

FreeMonoid

Definitions

Name	Category	Theorems
instStarMul 📖	CompOp	2 math math: star_one, star_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
star_of 📖	mathematical	—	Star.star FreeMonoid InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid instStarMul of	—	—
star_one 📖	mathematical	—	Star.star FreeMonoid InvolutiveStar.toStar StarMul.toInvolutiveStar MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid instStarMul MulOne.toOne	—	—

---

← Back to Index