Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-21 21:43 d3e20b4a

View on Github →

chore(data/multiset/basic): consistently use singleton notation (#8786)

Estimated changes

modified theorem multiset.gcd_singleton
modified theorem multiset.lcm_singleton
modified theorem finset.singleton_val
modified theorem multiset.antidiagonal_zero
modified theorem multiset.card_eq_one
modified theorem multiset.card_singleton
modified theorem multiset.count_singleton
modified theorem multiset.disjoint_singleton
modified theorem multiset.map_singleton
modified theorem multiset.mem_singleton
modified theorem multiset.mem_singleton_self
modified theorem multiset.prod_singleton
modified theorem multiset.product_singleton
modified theorem multiset.repeat_one
modified theorem multiset.singleton_add
modified theorem multiset.singleton_disjoint
modified theorem multiset.singleton_inj
modified theorem multiset.singleton_le
modified theorem multiset.singleton_ne_zero
modified theorem multiset.sum_map_singleton
modified theorem multiset.ndinsert_zero
modified theorem multiset.fold_singleton
modified theorem multiset.pure_def
modified theorem multiset.inf_singleton
modified theorem multiset.sup_singleton
modified theorem multiset.nodup_singleton
modified theorem multiset.pi_zero
modified theorem multiset.powerset_zero
modified theorem multiset.sections_zero
modified theorem polynomial.roots_X_sub_C