Commit 2023-05-28 11:05 6c01dc6e

View on Github →

refactor: use the typeclass SProd to implement overloaded notation · ×ˢ · (#4200) Currently, the following notations are changed from · ×ˢ · because Lean 4 can't deal with ambiguous notations. | Definition | Notation | | :

Estimated changes

modified theorem Subalgebra.coe_prod
modified theorem YoungDiagram.col_eq_prod
modified theorem YoungDiagram.row_eq_prod
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.Nonempty.fst
modified theorem Finset.Nonempty.product
modified theorem Finset.Nonempty.snd
modified theorem Finset.card_product
modified theorem Finset.diag_union_offDiag
modified theorem Finset.disjoint_product
modified theorem Finset.empty_product
modified theorem Finset.inter_product
modified theorem Finset.mem_product
modified theorem Finset.mk_mem_product
modified theorem Finset.nonempty_product
modified theorem Finset.offDiag_insert
modified theorem Finset.product_empty
modified theorem Finset.product_eq_empty
modified theorem Finset.product_image_fst
modified theorem Finset.product_image_snd
modified theorem Finset.product_inter
modified theorem Finset.product_sdiff_diag
modified theorem Finset.product_singleton
modified theorem Finset.product_union
modified theorem Finset.product_val
modified theorem Finset.union_product
modified theorem Finset.image_inf_product
modified theorem Finset.image_sup_product
modified theorem List.nil_product
modified theorem List.product_nil
modified theorem Multiset.card_product
modified theorem Multiset.coe_product
modified theorem Multiset.cons_product
modified theorem Multiset.product_cons
modified theorem Multiset.product_zero
modified theorem Multiset.zero_product
modified theorem Subgroup.coe_prod
modified theorem Submonoid.coe_prod
modified theorem Subsemigroup.coe_prod
modified theorem Submodule.prod_coe
modified theorem Filter.mem_prod_self_iff
modified theorem Filter.prod_same_eq
modified theorem Filter.map₂_mk_eq_prod
modified theorem Filter.one_prod_one
modified theorem Filter.NeBot.prod
modified theorem Filter.bot_prod
modified theorem Filter.inf_prod
modified theorem Filter.le_prod_map_fst_snd
modified theorem Filter.map_fst_prod
modified theorem Filter.map_snd_prod
modified theorem Filter.prod_bot
modified theorem Filter.prod_comm'
modified theorem Filter.prod_comm
modified theorem Filter.prod_eq
modified theorem Filter.prod_eq_bot
modified theorem Filter.prod_inf
modified theorem Filter.prod_mono_left
modified theorem Filter.prod_mono_right
modified theorem Filter.prod_neBot
modified theorem Filter.prod_pure
modified theorem Filter.prod_pure_pure
modified theorem Filter.prod_sup
modified theorem Filter.prod_top
modified theorem Filter.pure_prod
modified theorem Filter.sup_prod
modified theorem Filter.tendsto_diag
modified theorem Filter.tendsto_fst
modified theorem Filter.tendsto_snd
modified theorem LowerSet.Ici_prod_Ici
modified theorem LowerSet.Iic_prod
modified theorem LowerSet.bot_prod
modified theorem LowerSet.coe_prod
modified theorem LowerSet.disjoint_prod
modified theorem LowerSet.inf_prod
modified theorem LowerSet.mem_prod
modified theorem LowerSet.prod_bot
modified theorem LowerSet.prod_eq_bot
modified theorem LowerSet.prod_inf
modified theorem LowerSet.prod_inf_prod
modified theorem LowerSet.prod_le_prod_iff
modified theorem LowerSet.prod_mono
modified theorem LowerSet.prod_mono_left
modified theorem LowerSet.prod_mono_right
modified theorem LowerSet.prod_sup
modified theorem LowerSet.sup_prod
modified theorem LowerSet.top_prod_top
modified theorem UpperSet.Ici_prod
modified theorem UpperSet.Ici_prod_Ici
modified theorem UpperSet.bot_prod_bot
modified theorem UpperSet.coe_prod
modified theorem UpperSet.inf_prod
modified theorem UpperSet.mem_prod
modified theorem UpperSet.prod_eq_top
modified theorem UpperSet.prod_inf
modified theorem UpperSet.prod_le_prod_iff
modified theorem UpperSet.prod_mono
modified theorem UpperSet.prod_mono_left
modified theorem UpperSet.prod_mono_right
modified theorem UpperSet.prod_sup
modified theorem UpperSet.prod_sup_prod
modified theorem UpperSet.prod_top
modified theorem UpperSet.sup_prod
modified theorem UpperSet.top_prod
modified theorem Subring.coe_prod
modified theorem Subsemiring.coe_prod
modified theorem OpenSubgroup.coe_prod
modified theorem nhds_prod_eq