Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-12 09:58 f1944b30

View on Github →

refactor(*): Extend ×ˢ notation (#15717) Delete has_set_prod in favor of a direct notation declaration. Overload that notation with the list, finset, multiset versions. Use the new notation and remove type ascriptions to the existing uses where possible (because Lean gets more information from the notation now).

Estimated changes

modified theorem subalgebra.coe_prod
modified def rel.interedges
modified theorem finset.div_def
modified theorem finset.image_div_prod
modified theorem finset.image_mul_product
modified theorem finset.image_smul_product
modified theorem finset.mul_def
modified theorem finset.smul_def
modified theorem finset.card_product
modified def finset.diag
modified theorem finset.diag_union_off_diag
modified theorem finset.empty_product
modified theorem finset.mem_product
modified theorem finset.mk_mem_product
modified theorem finset.nonempty.fst
modified theorem finset.nonempty.product
modified theorem finset.nonempty.snd
modified theorem finset.nonempty_product
modified def finset.off_diag
modified theorem finset.product_empty
modified theorem finset.product_eq_empty
modified theorem finset.product_sdiff_diag
modified theorem finset.product_val
modified theorem multiset.add_product
modified theorem multiset.card_product
modified theorem multiset.cons_product
modified theorem multiset.product_add
modified theorem multiset.product_singleton
modified theorem set.nonempty.fst
modified theorem set.nonempty.prod
modified theorem set.nonempty.snd
added def set.prod
modified theorem set.prod_nonempty_iff
modified theorem subgroup.coe_prod
modified theorem submonoid.coe_prod
modified theorem subsemigroup.coe_prod
modified theorem submodule.prod_coe
modified theorem region_between_subset
modified theorem subring.coe_prod
modified theorem subsemiring.coe_prod
modified theorem witt_vector.witt_add_vars
modified theorem witt_vector.witt_mul_vars
modified theorem witt_vector.witt_neg_vars
modified theorem witt_vector.witt_sub_vars
modified theorem witt_vector.remainder_vars