Commit 2023-01-11 19:03 8484c193

View on Github →

feat port: Algebra.FreeMonoid.Count (#1483) It necessary to use Bool instead of Prop to match the changes made in List.countp so I add to change some if to bif at a couple of places.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/FreeMonoid/Count.lean

added def FreeAddMonoid.count

added theorem FreeAddMonoid.count_apply

added theorem FreeAddMonoid.count_of

added def FreeAddMonoid.countp

added theorem FreeAddMonoid.countp_apply

added theorem FreeAddMonoid.countp_of

added def FreeMonoid.count

added theorem FreeMonoid.count_apply

added theorem FreeMonoid.count_of

added def FreeMonoid.countp

added theorem FreeMonoid.countp_apply

added theorem FreeMonoid.countp_of'

added theorem FreeMonoid.countp_of