Commit 2023-01-21 16:25 e5a64715

View on Github →

feat: Port Algebra.Support (#1747)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Support.lean

added theorem Function.compl_mulSupport

added theorem Function.disjoint_mulSupport_iff

added theorem Function.mem_mulSupport

added def Function.mulSupport

added theorem Function.mulSupport_add_one'

added theorem Function.mulSupport_add_one

added theorem Function.mulSupport_along_fiber_finite_of_finite

added theorem Function.mulSupport_along_fiber_subset

added theorem Function.mulSupport_binop_subset

added theorem Function.mulSupport_comp_eq

added theorem Function.mulSupport_comp_eq_preimage

added theorem Function.mulSupport_comp_subset

added theorem Function.mulSupport_const

added theorem Function.mulSupport_disjoint_iff

added theorem Function.mulSupport_div

added theorem Function.mulSupport_eq_empty_iff

added theorem Function.mulSupport_eq_iff

added theorem Function.mulSupport_eq_preimage

added theorem Function.mulSupport_inf

added theorem Function.mulSupport_infᵢ

added theorem Function.mulSupport_inv'

added theorem Function.mulSupport_inv

added theorem Function.mulSupport_max

added theorem Function.mulSupport_min

added theorem Function.mulSupport_mul

added theorem Function.mulSupport_mul_inv

added theorem Function.mulSupport_nonempty_iff

added theorem Function.mulSupport_one'

added theorem Function.mulSupport_one

added theorem Function.mulSupport_one_add'

added theorem Function.mulSupport_one_add

added theorem Function.mulSupport_one_sub'

added theorem Function.mulSupport_one_sub

added theorem Function.mulSupport_pow

added theorem Function.mulSupport_prod

added theorem Function.mulSupport_prod_mk'

added theorem Function.mulSupport_prod_mk

added theorem Function.mulSupport_subset_comp

added theorem Function.mulSupport_subset_iff'

added theorem Function.mulSupport_subset_iff

added theorem Function.mulSupport_sup

added theorem Function.mulSupport_supᵢ

added theorem Function.nmem_mulSupport

added theorem Function.range_subset_insert_image_mulSupport

added def Function.support

added theorem Function.support_const_smul_of_ne_zero

added theorem Function.support_div

added theorem Function.support_inv

added theorem Function.support_mul

added theorem Function.support_mul_subset_left

added theorem Function.support_mul_subset_right

added theorem Function.support_prod

added theorem Function.support_prod_subset

added theorem Function.support_smul

added theorem Function.support_smul_subset_left

added theorem Function.support_smul_subset_right

added theorem Pi.mulSupport_mulSingle

added theorem Pi.mulSupport_mulSingle_disjoint

added theorem Pi.mulSupport_mulSingle_of_ne

added theorem Pi.mulSupport_mulSingle_one

added theorem Pi.mulSupport_mulSingle_subset

added theorem Set.image_inter_mulSupport_eq