Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-13 19:48 fde3d78c

View on Github →

chore(multiset): dedicated notation for multiset.cons (#4600)

Estimated changes

modified theorem finset.cons_val
modified theorem finset.insert_val'
modified theorem finset.mk_cons
modified theorem finset.singleton_val
modified theorem multiset.antidiagonal_cons
modified theorem multiset.antidiagonal_zero
modified theorem multiset.add_cons
modified theorem multiset.card_cons
modified theorem multiset.card_eq_one
modified theorem multiset.card_singleton
modified theorem multiset.cons_add
modified theorem multiset.cons_bind
modified theorem multiset.cons_erase
modified theorem multiset.cons_inj_right
modified theorem multiset.cons_inter_distrib
modified theorem multiset.cons_le_cons
modified theorem multiset.cons_le_cons_iff
modified theorem multiset.cons_ne_zero
modified theorem multiset.cons_subset
modified theorem multiset.cons_swap
modified theorem multiset.cons_union_distrib
modified theorem multiset.count_cons_of_ne
modified theorem multiset.count_cons_self
modified theorem multiset.count_singleton
modified theorem multiset.countp_cons_of_neg
modified theorem multiset.countp_cons_of_pos
modified theorem multiset.disjoint_singleton
modified theorem multiset.erase_cons_head
modified theorem multiset.erase_cons_tail
modified theorem multiset.exists_cons_of_mem
modified theorem multiset.filter_cons_of_neg
modified theorem multiset.filter_cons_of_pos
modified theorem multiset.foldl_cons
modified theorem multiset.foldr_cons
modified theorem multiset.join_cons
modified theorem multiset.le_cons_erase
modified theorem multiset.le_cons_of_not_mem
modified theorem multiset.le_cons_self
modified theorem multiset.lt_cons_self
modified theorem multiset.lt_iff_cons_le
modified theorem multiset.map_cons
modified theorem multiset.mem_cons
modified theorem multiset.mem_cons_of_mem
modified theorem multiset.mem_cons_self
modified theorem multiset.mem_singleton
modified theorem multiset.mem_singleton_self
modified theorem multiset.prod_cons
modified theorem multiset.prod_singleton
modified theorem multiset.product_singleton
modified theorem multiset.repeat_one
modified theorem multiset.repeat_succ
modified theorem multiset.singleton_add
modified theorem multiset.singleton_coe
modified theorem multiset.singleton_disjoint
modified theorem multiset.singleton_inj
modified theorem multiset.singleton_le
modified theorem multiset.singleton_ne_zero
modified theorem multiset.sub_cons
modified theorem multiset.zero_ne_cons
modified theorem multiset.ndinsert_zero
modified theorem multiset.fold_cons'_left
modified theorem multiset.fold_cons'_right
modified theorem multiset.fold_cons_right
modified theorem multiset.fold_singleton
modified theorem multiset.pure_def
modified theorem multiset.gcd_singleton
modified theorem multiset.lcm_singleton
modified theorem multiset.Ico.eq_cons
modified theorem multiset.Ico.succ_top
modified theorem multiset.inf_singleton
modified theorem multiset.sup_singleton
modified theorem multiset.nodup_cons
modified theorem multiset.nodup_iff_le
modified theorem multiset.nodup_singleton
modified theorem multiset.not_nodup_pair
modified def multiset.pi.cons
modified theorem multiset.pi.cons_same
modified theorem multiset.pi_zero
modified theorem multiset.powerset_zero
modified theorem multiset.range_succ
modified theorem multiset.sections_zero
modified theorem polynomial.roots_X_sub_C