Count

📁 Source: Mathlib/Algebra/FreeMonoid/Count.lean

Statistics

Metric	Count
Definitions count, countP, countP', count, countP, countP'	6
Theorems countP'_add, countP'_zero, countP_apply, countP_of, count_apply, count_of, countP'_mul, countP'_one, countP_apply, countP_of, count_apply, count_of	12
Total	18

FreeAddMonoid

Definitions

Name	Category	Theorems
count 📖	CompOp	2 math math: count_apply, count_of
countP 📖	CompOp	2 math math: countP_apply, countP_of
countP' 📖	CompOp	2 math math: countP'_add, countP'_zero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countP'_add 📖	mathematical	—	countP' FreeAddMonoid AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid	—	—
countP'_zero 📖	mathematical	—	countP' FreeAddMonoid AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid	—	—
countP_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom FreeAddMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid Nat.instAddMonoid AddMonoidHom.instFunLike countP Equiv EquivLike.toFunLike Equiv.instEquivLike toList	—	—
countP_of 📖	mathematical	—	DFunLike.coe AddMonoidHom FreeAddMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid Nat.instAddMonoid AddMonoidHom.instFunLike countP of	—	countP_apply toList_of
count_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom FreeAddMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid Nat.instAddMonoid AddMonoidHom.instFunLike count Equiv EquivLike.toFunLike Equiv.instEquivLike toList	—	—
count_of 📖	mathematical	—	DFunLike.coe AddMonoidHom FreeAddMonoid AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddRightCancelMonoid.toAddMonoid AddCancelMonoid.toAddRightCancelMonoid instAddCancelMonoid Nat.instAddMonoid AddMonoidHom.instFunLike count of Pi.single AddZero.toZero	—	countP_of

FreeMonoid

Definitions

Name	Category	Theorems
count 📖	CompOp	2 math math: count_of, count_apply
countP 📖	CompOp	2 math math: countP_of, countP_apply
countP' 📖	CompOp	2 math math: countP'_mul, countP'_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
countP'_mul 📖	mathematical	—	countP' FreeMonoid MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid	—	—
countP'_one 📖	mathematical	—	countP' FreeMonoid MulOne.toOne MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid	—	—
countP_apply 📖	mathematical	—	DFunLike.coe MonoidHom FreeMonoid Multiplicative MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid Multiplicative.mulOneClass AddMonoid.toAddZeroClass Nat.instAddMonoid MonoidHom.instFunLike countP Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd toList	—	—
countP_of 📖	mathematical	—	DFunLike.coe MonoidHom FreeMonoid Multiplicative MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid Multiplicative.mulOneClass AddMonoid.toAddZeroClass Nat.instAddMonoid MonoidHom.instFunLike countP of Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	countP_apply toList_of
count_apply 📖	mathematical	—	DFunLike.coe MonoidHom FreeMonoid Multiplicative MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid Multiplicative.mulOneClass AddMonoid.toAddZeroClass Nat.instAddMonoid MonoidHom.instFunLike count Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd FreeAddMonoid FreeAddMonoid.toList	—	—
count_of 📖	mathematical	—	DFunLike.coe MonoidHom FreeMonoid Multiplicative MulOneClass.toMulOne Monoid.toMulOneClass RightCancelMonoid.toMonoid CancelMonoid.toRightCancelMonoid instCancelMonoid Multiplicative.mulOneClass AddMonoid.toAddZeroClass Nat.instAddMonoid MonoidHom.instFunLike count of Pi.mulSingle instOneMultiplicativeOfZero AddZero.toZero AddZeroClass.toAddZero Equiv EquivLike.toFunLike Equiv.instEquivLike Multiplicative.ofAdd	—	countP_of Pi.mulSingle_apply

---

← Back to Index