Commit 2023-08-23 00:18 f59eee0e

View on Github →

chore: bump Std (#6721) This incorporates changes from https://github.com/leanprover-community/mathlib4/pull/6575 I have also renamed Multiset.countp to Multiset.countP for consistency.

Estimated changes

modified def FreeAddMonoid.count
deleted theorem FreeAddMonoid.countp_of
modified def FreeMonoid.count
added theorem FreeMonoid.countP_of'
added theorem FreeMonoid.countP_of
deleted def FreeMonoid.countp
deleted theorem FreeMonoid.countp_apply
deleted theorem FreeMonoid.countp_of'
deleted theorem FreeMonoid.countp_of
deleted theorem List.Sublist.count_le
deleted theorem List.Sublist.countp_le
added theorem List.countP_join
deleted theorem List.count_append
deleted theorem List.count_concat
modified theorem List.count_cons'
deleted theorem List.count_cons
deleted theorem List.count_cons_of_ne
deleted theorem List.count_cons_self
deleted theorem List.count_eq_length
deleted theorem List.count_eq_zero
deleted theorem List.count_erase
deleted theorem List.count_erase_of_ne
deleted theorem List.count_erase_self
deleted theorem List.count_filter
deleted theorem List.count_le_count_cons
deleted theorem List.count_le_count_map
deleted theorem List.count_le_length
deleted theorem List.count_nil
deleted theorem List.count_pos
deleted theorem List.count_replicate
deleted theorem List.count_replicate_self
deleted theorem List.count_singleton'
deleted theorem List.count_singleton
deleted theorem List.count_tail
deleted theorem List.countp_append
deleted theorem List.countp_congr
deleted theorem List.countp_cons
deleted theorem List.countp_cons_of_neg
deleted theorem List.countp_cons_of_pos
deleted theorem List.countp_eq_length
deleted theorem List.countp_eq_zero
deleted theorem List.countp_false
deleted theorem List.countp_filter
deleted theorem List.countp_join
deleted theorem List.countp_le_length
deleted theorem List.countp_map
deleted theorem List.countp_mono_left
deleted theorem List.countp_nil
deleted theorem List.countp_pos
deleted theorem List.countp_true
deleted theorem List.filter_beq'
deleted theorem List.filter_beq
deleted theorem List.filter_eq'
deleted theorem List.filter_eq
deleted theorem List.one_le_count_iff_mem
added theorem List.Perm.countP_congr
added theorem List.Perm.countP_eq
deleted theorem List.Perm.countp_congr
deleted theorem List.Perm.countp_eq
added theorem List.Subperm.countP_le
deleted theorem List.Subperm.countp_le
added theorem Multiset.Rel.countP_eq
deleted theorem Multiset.Rel.countp_eq
added theorem Multiset.coe_countP
deleted theorem Multiset.coe_countp
added def Multiset.countP
added theorem Multiset.countP_False
added theorem Multiset.countP_True
added theorem Multiset.countP_add
added theorem Multiset.countP_congr
added theorem Multiset.countP_cons
added theorem Multiset.countP_filter
added theorem Multiset.countP_map
added theorem Multiset.countP_nsmul
added theorem Multiset.countP_pos
added theorem Multiset.countP_sub
added theorem Multiset.countP_zero
modified theorem Multiset.count_pos
deleted def Multiset.countp
deleted theorem Multiset.countp_False
deleted theorem Multiset.countp_True
deleted theorem Multiset.countp_add
deleted theorem Multiset.countp_congr
deleted theorem Multiset.countp_cons
deleted theorem Multiset.countp_eq_card
deleted theorem Multiset.countp_eq_zero
deleted theorem Multiset.countp_filter
deleted theorem Multiset.countp_le_card
deleted theorem Multiset.countp_le_of_le
deleted theorem Multiset.countp_map
deleted theorem Multiset.countp_nsmul
deleted theorem Multiset.countp_pos
deleted theorem Multiset.countp_sub
deleted theorem Multiset.countp_zero
deleted def getInitHeartbeats
deleted def getMaxHeartbeats
deleted def heartbeatsPercent