Commit 2023-07-12 02:40 268b7d43

View on Github →

chore: rename Dfinsupp to DFinsupp (#5822) See #4354

Estimated changes

Modified Counterexamples/DirectSumIsInternal.lean

Modified Counterexamples/HomogeneousPrimeNotPrime.lean

Modified Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

Modified Mathlib.lean

Modified Mathlib/Algebra/DirectLimit.lean

Modified Mathlib/Algebra/DirectSum/Algebra.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/DirectSum/Finsupp.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

modified theorem DirectSum.single_eq_lof

Modified Mathlib/Algebra/DirectSum/Ring.lean

Modified Mathlib/Algebra/Lie/DirectSum.lean

Modified Mathlib/Algebra/Module/PID.lean

Modified Mathlib/Algebra/Module/Projective.lean

Modified Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

added theorem DFinsupp.inner_sum

added theorem DFinsupp.sum_inner

deleted theorem Dfinsupp.inner_sum

deleted theorem Dfinsupp.sum_inner

Modified Mathlib/Analysis/InnerProductSpace/PiL2.lean

Modified Mathlib/Analysis/InnerProductSpace/Projection.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Renamed Mathlib/Data/Dfinsupp/Basic.lean to Mathlib/Data/DFinsupp/Basic.lean

added theorem DFinsupp.addHom_ext'

added theorem DFinsupp.addHom_ext

added theorem DFinsupp.add_apply

added theorem DFinsupp.add_closure_iUnion_range_single

added def DFinsupp.coeFnAddMonoidHom

added theorem DFinsupp.coeFn_injective

added theorem DFinsupp.coe_add

added theorem DFinsupp.coe_finset_sum

added theorem DFinsupp.coe_mk'

added theorem DFinsupp.coe_neg

added theorem DFinsupp.coe_nsmul

added theorem DFinsupp.coe_piecewise

added theorem DFinsupp.coe_smul

added theorem DFinsupp.coe_sub

added theorem DFinsupp.coe_update

added theorem DFinsupp.coe_zero

added theorem DFinsupp.coe_zsmul

added def DFinsupp.comapDomain'

added theorem DFinsupp.comapDomain'_add

added theorem DFinsupp.comapDomain'_apply

added theorem DFinsupp.comapDomain'_single

added theorem DFinsupp.comapDomain'_smul

added theorem DFinsupp.comapDomain'_zero

added theorem DFinsupp.comapDomain_add

added theorem DFinsupp.comapDomain_apply

added theorem DFinsupp.comapDomain_single

added theorem DFinsupp.comapDomain_smul

added theorem DFinsupp.comapDomain_zero

added theorem DFinsupp.comp_liftAddHom

added theorem DFinsupp.comp_sumAddHom

added theorem DFinsupp.eq_mk_support

added def DFinsupp.equivCongrLeft

added def DFinsupp.equivFunOnFintype

added theorem DFinsupp.equivFunOnFintype_single

added theorem DFinsupp.equivFunOnFintype_symm_coe

added theorem DFinsupp.equivFunOnFintype_symm_single

added theorem DFinsupp.equivProdDFinsupp_add

added theorem DFinsupp.equivProdDFinsupp_smul

added def DFinsupp.erase

added def DFinsupp.eraseAddHom

added theorem DFinsupp.erase_add

added theorem DFinsupp.erase_add_single

added theorem DFinsupp.erase_apply

added theorem DFinsupp.erase_def

added theorem DFinsupp.erase_eq_sub_single

added theorem DFinsupp.erase_ne

added theorem DFinsupp.erase_neg

added theorem DFinsupp.erase_same

added theorem DFinsupp.erase_single

added theorem DFinsupp.erase_single_ne

added theorem DFinsupp.erase_single_same

added theorem DFinsupp.erase_sub

added theorem DFinsupp.erase_zero

added def DFinsupp.evalAddMonoidHom

added theorem DFinsupp.ext

added theorem DFinsupp.ext_iff

added def DFinsupp.extendWith

added theorem DFinsupp.extendWith_none

added theorem DFinsupp.extendWith_single_zero

added theorem DFinsupp.extendWith_some

added theorem DFinsupp.extendWith_zero

added def DFinsupp.filter

added def DFinsupp.filterAddMonoidHom

added def DFinsupp.filterLinearMap

added theorem DFinsupp.filter_add

added theorem DFinsupp.filter_apply

added theorem DFinsupp.filter_apply_neg

added theorem DFinsupp.filter_apply_pos

added theorem DFinsupp.filter_def

added theorem DFinsupp.filter_ne_eq_erase'

added theorem DFinsupp.filter_ne_eq_erase

added theorem DFinsupp.filter_neg

added theorem DFinsupp.filter_pos_add_filter_neg

added theorem DFinsupp.filter_single

added theorem DFinsupp.filter_single_neg

added theorem DFinsupp.filter_single_pos

added theorem DFinsupp.filter_smul

added theorem DFinsupp.filter_sub

added theorem DFinsupp.filter_zero

added theorem DFinsupp.finite_support

added theorem DFinsupp.finset_sum_apply

added theorem DFinsupp.induction₂

added theorem DFinsupp.infinite_of_exists_right

added def DFinsupp.liftAddHom

added theorem DFinsupp.liftAddHom_apply_single

added theorem DFinsupp.liftAddHom_comp_single

added theorem DFinsupp.liftAddHom_singleAddHom

added def DFinsupp.mapRange.addEquiv

added theorem DFinsupp.mapRange.addEquiv_refl

added theorem DFinsupp.mapRange.addEquiv_symm

added theorem DFinsupp.mapRange.addEquiv_trans

added def DFinsupp.mapRange.addMonoidHom

added theorem DFinsupp.mapRange.addMonoidHom_comp

added theorem DFinsupp.mapRange.addMonoidHom_id

added def DFinsupp.mapRange

added theorem DFinsupp.mapRange_add

added theorem DFinsupp.mapRange_apply

added theorem DFinsupp.mapRange_comp

added theorem DFinsupp.mapRange_def

added theorem DFinsupp.mapRange_id

added theorem DFinsupp.mapRange_single

added theorem DFinsupp.mapRange_zero

added theorem DFinsupp.mem_support_iff

added theorem DFinsupp.mem_support_toFun

added def DFinsupp.mk

added def DFinsupp.mkAddGroupHom

added theorem DFinsupp.mk_add

added theorem DFinsupp.mk_apply

added theorem DFinsupp.mk_injective

added theorem DFinsupp.mk_neg

added theorem DFinsupp.mk_of_mem

added theorem DFinsupp.mk_of_not_mem

added theorem DFinsupp.mk_smul

added theorem DFinsupp.mk_sub

added theorem DFinsupp.mk_zero

added theorem DFinsupp.neg_apply

added theorem DFinsupp.not_mem_support_iff

added theorem DFinsupp.nsmul_apply

added def DFinsupp.piecewise

added theorem DFinsupp.piecewise_apply

added theorem DFinsupp.piecewise_single_erase

added def DFinsupp.prod

added theorem DFinsupp.prod_add_index

added theorem DFinsupp.prod_comm

added theorem DFinsupp.prod_eq_one

added theorem DFinsupp.prod_eq_prod_fintype

added theorem DFinsupp.prod_finset_sum_index

added theorem DFinsupp.prod_inv

added theorem DFinsupp.prod_mapRange_index

added theorem DFinsupp.prod_mul

added theorem DFinsupp.prod_neg_index

added theorem DFinsupp.prod_one

added theorem DFinsupp.prod_single_index

added theorem DFinsupp.prod_subtypeDomain_index

added theorem DFinsupp.prod_sum_index

added theorem DFinsupp.prod_zero_index

added theorem DFinsupp.sigmaCurry_add

added theorem DFinsupp.sigmaCurry_apply

added theorem DFinsupp.sigmaCurry_single

added theorem DFinsupp.sigmaCurry_smul

added theorem DFinsupp.sigmaCurry_zero

added def DFinsupp.sigmaUncurry

added theorem DFinsupp.sigmaUncurry_add

added theorem DFinsupp.sigmaUncurry_apply

added theorem DFinsupp.sigmaUncurry_single

added theorem DFinsupp.sigmaUncurry_smul

added theorem DFinsupp.sigmaUncurry_zero

added def DFinsupp.single

added def DFinsupp.singleAddHom

added theorem DFinsupp.single_add

added theorem DFinsupp.single_add_erase

added theorem DFinsupp.single_apply

added theorem DFinsupp.single_eq_of_ne

added theorem DFinsupp.single_eq_of_sigma_eq

added theorem DFinsupp.single_eq_pi_single

added theorem DFinsupp.single_eq_same

added theorem DFinsupp.single_eq_single_iff

added theorem DFinsupp.single_eq_zero

added theorem DFinsupp.single_injective

added theorem DFinsupp.single_left_injective

added theorem DFinsupp.single_neg

added theorem DFinsupp.single_smul

added theorem DFinsupp.single_sub

added theorem DFinsupp.single_zero

added theorem DFinsupp.smul_apply

added theorem DFinsupp.smul_sum

added theorem DFinsupp.sub_apply

added def DFinsupp.subtypeDomain

added def DFinsupp.subtypeDomainAddMonoidHom

added def DFinsupp.subtypeDomainLinearMap

added theorem DFinsupp.subtypeDomain_add

added theorem DFinsupp.subtypeDomain_apply

added theorem DFinsupp.subtypeDomain_def

added theorem DFinsupp.subtypeDomain_finsupp_sum

added theorem DFinsupp.subtypeDomain_neg

added theorem DFinsupp.subtypeDomain_smul

added theorem DFinsupp.subtypeDomain_sub

added theorem DFinsupp.subtypeDomain_sum

added theorem DFinsupp.subtypeDomain_zero

added def DFinsupp.sumAddHom

added theorem DFinsupp.sumAddHom_add

added theorem DFinsupp.sumAddHom_apply

added theorem DFinsupp.sumAddHom_comm

added theorem DFinsupp.sumAddHom_comp_single

added theorem DFinsupp.sumAddHom_single

added theorem DFinsupp.sumAddHom_singleAddHom

added theorem DFinsupp.sumAddHom_zero

added theorem DFinsupp.sum_apply

added theorem DFinsupp.sum_single

added theorem DFinsupp.sum_sub_index

added def DFinsupp.support

added theorem DFinsupp.support_add

added theorem DFinsupp.support_eq_empty

added theorem DFinsupp.support_erase

added theorem DFinsupp.support_filter

added theorem DFinsupp.support_mapRange

added theorem DFinsupp.support_mk'_subset

added theorem DFinsupp.support_mk_subset

added theorem DFinsupp.support_neg

added theorem DFinsupp.support_single_ne_zero

added theorem DFinsupp.support_single_subset

added theorem DFinsupp.support_smul

added theorem DFinsupp.support_subset_iff

added theorem DFinsupp.support_subtypeDomain

added theorem DFinsupp.support_sum

added theorem DFinsupp.support_update

added theorem DFinsupp.support_update_ne_zero

added theorem DFinsupp.support_zero

added theorem DFinsupp.support_zipWith

added theorem DFinsupp.toFun_eq_coe

added def DFinsupp.update

added theorem DFinsupp.update_eq_erase

added theorem DFinsupp.update_eq_erase_add_single

added theorem DFinsupp.update_eq_single_add_erase

added theorem DFinsupp.update_eq_sub_add_single

added theorem DFinsupp.update_self

added theorem DFinsupp.zero_apply

added def DFinsupp.zipWith

added theorem DFinsupp.zipWith_apply

added theorem DFinsupp.zipWith_def

added theorem DFinsupp.zsmul_apply

added structure DFinsupp

deleted theorem Dfinsupp.addHom_ext'

deleted theorem Dfinsupp.addHom_ext

deleted theorem Dfinsupp.add_apply

deleted theorem Dfinsupp.add_closure_iUnion_range_single

deleted def Dfinsupp.coeFnAddMonoidHom

deleted theorem Dfinsupp.coeFn_injective

deleted theorem Dfinsupp.coe_add

deleted theorem Dfinsupp.coe_finset_sum

deleted theorem Dfinsupp.coe_mk'

deleted theorem Dfinsupp.coe_neg

deleted theorem Dfinsupp.coe_nsmul

deleted theorem Dfinsupp.coe_piecewise

deleted theorem Dfinsupp.coe_smul

deleted theorem Dfinsupp.coe_sub

deleted theorem Dfinsupp.coe_update

deleted theorem Dfinsupp.coe_zero

deleted theorem Dfinsupp.coe_zsmul

deleted def Dfinsupp.comapDomain'

deleted theorem Dfinsupp.comapDomain'_add

deleted theorem Dfinsupp.comapDomain'_apply

deleted theorem Dfinsupp.comapDomain'_single

deleted theorem Dfinsupp.comapDomain'_smul

deleted theorem Dfinsupp.comapDomain'_zero

deleted theorem Dfinsupp.comapDomain_add

deleted theorem Dfinsupp.comapDomain_apply

deleted theorem Dfinsupp.comapDomain_single

deleted theorem Dfinsupp.comapDomain_smul

deleted theorem Dfinsupp.comapDomain_zero

deleted theorem Dfinsupp.comp_liftAddHom

deleted theorem Dfinsupp.comp_sumAddHom

deleted theorem Dfinsupp.eq_mk_support

deleted def Dfinsupp.equivCongrLeft

deleted def Dfinsupp.equivFunOnFintype

deleted theorem Dfinsupp.equivFunOnFintype_single

deleted theorem Dfinsupp.equivFunOnFintype_symm_coe

deleted theorem Dfinsupp.equivFunOnFintype_symm_single

deleted theorem Dfinsupp.equivProdDfinsupp_add

deleted theorem Dfinsupp.equivProdDfinsupp_smul

deleted def Dfinsupp.erase

deleted def Dfinsupp.eraseAddHom

deleted theorem Dfinsupp.erase_add

deleted theorem Dfinsupp.erase_add_single

deleted theorem Dfinsupp.erase_apply

deleted theorem Dfinsupp.erase_def

deleted theorem Dfinsupp.erase_eq_sub_single

deleted theorem Dfinsupp.erase_ne

deleted theorem Dfinsupp.erase_neg

deleted theorem Dfinsupp.erase_same

deleted theorem Dfinsupp.erase_single

deleted theorem Dfinsupp.erase_single_ne

deleted theorem Dfinsupp.erase_single_same

deleted theorem Dfinsupp.erase_sub

deleted theorem Dfinsupp.erase_zero

deleted def Dfinsupp.evalAddMonoidHom

deleted theorem Dfinsupp.ext

deleted theorem Dfinsupp.ext_iff

deleted def Dfinsupp.extendWith

deleted theorem Dfinsupp.extendWith_none

deleted theorem Dfinsupp.extendWith_single_zero

deleted theorem Dfinsupp.extendWith_some

deleted theorem Dfinsupp.extendWith_zero

deleted def Dfinsupp.filter

deleted def Dfinsupp.filterAddMonoidHom

deleted def Dfinsupp.filterLinearMap

deleted theorem Dfinsupp.filter_add

deleted theorem Dfinsupp.filter_apply

deleted theorem Dfinsupp.filter_apply_neg

deleted theorem Dfinsupp.filter_apply_pos

deleted theorem Dfinsupp.filter_def

deleted theorem Dfinsupp.filter_ne_eq_erase'

deleted theorem Dfinsupp.filter_ne_eq_erase

deleted theorem Dfinsupp.filter_neg

deleted theorem Dfinsupp.filter_pos_add_filter_neg

deleted theorem Dfinsupp.filter_single

deleted theorem Dfinsupp.filter_single_neg

deleted theorem Dfinsupp.filter_single_pos

deleted theorem Dfinsupp.filter_smul

deleted theorem Dfinsupp.filter_sub

deleted theorem Dfinsupp.filter_zero

deleted theorem Dfinsupp.finite_support

deleted theorem Dfinsupp.finset_sum_apply

deleted theorem Dfinsupp.induction₂

deleted theorem Dfinsupp.infinite_of_exists_right

deleted def Dfinsupp.liftAddHom

deleted theorem Dfinsupp.liftAddHom_apply_single

deleted theorem Dfinsupp.liftAddHom_comp_single

deleted theorem Dfinsupp.liftAddHom_singleAddHom

deleted def Dfinsupp.mapRange.addEquiv

deleted theorem Dfinsupp.mapRange.addEquiv_refl

deleted theorem Dfinsupp.mapRange.addEquiv_symm

deleted theorem Dfinsupp.mapRange.addEquiv_trans

deleted def Dfinsupp.mapRange.addMonoidHom

deleted theorem Dfinsupp.mapRange.addMonoidHom_comp

deleted theorem Dfinsupp.mapRange.addMonoidHom_id

deleted def Dfinsupp.mapRange

deleted theorem Dfinsupp.mapRange_add

deleted theorem Dfinsupp.mapRange_apply

deleted theorem Dfinsupp.mapRange_comp

deleted theorem Dfinsupp.mapRange_def

deleted theorem Dfinsupp.mapRange_id

deleted theorem Dfinsupp.mapRange_single

deleted theorem Dfinsupp.mapRange_zero

deleted theorem Dfinsupp.mem_support_iff

deleted theorem Dfinsupp.mem_support_toFun

deleted def Dfinsupp.mk

deleted def Dfinsupp.mkAddGroupHom

deleted theorem Dfinsupp.mk_add

deleted theorem Dfinsupp.mk_apply

deleted theorem Dfinsupp.mk_injective

deleted theorem Dfinsupp.mk_neg

deleted theorem Dfinsupp.mk_of_mem

deleted theorem Dfinsupp.mk_of_not_mem

deleted theorem Dfinsupp.mk_smul

deleted theorem Dfinsupp.mk_sub

deleted theorem Dfinsupp.mk_zero

deleted theorem Dfinsupp.neg_apply

deleted theorem Dfinsupp.not_mem_support_iff

deleted theorem Dfinsupp.nsmul_apply

deleted def Dfinsupp.piecewise

deleted theorem Dfinsupp.piecewise_apply

deleted theorem Dfinsupp.piecewise_single_erase

deleted def Dfinsupp.prod

deleted theorem Dfinsupp.prod_add_index

deleted theorem Dfinsupp.prod_comm

deleted theorem Dfinsupp.prod_eq_one

deleted theorem Dfinsupp.prod_eq_prod_fintype

deleted theorem Dfinsupp.prod_finset_sum_index

deleted theorem Dfinsupp.prod_inv

deleted theorem Dfinsupp.prod_mapRange_index

deleted theorem Dfinsupp.prod_mul

deleted theorem Dfinsupp.prod_neg_index

deleted theorem Dfinsupp.prod_one

deleted theorem Dfinsupp.prod_single_index

deleted theorem Dfinsupp.prod_subtypeDomain_index

deleted theorem Dfinsupp.prod_sum_index

deleted theorem Dfinsupp.prod_zero_index

deleted theorem Dfinsupp.sigmaCurry_add

deleted theorem Dfinsupp.sigmaCurry_apply

deleted theorem Dfinsupp.sigmaCurry_single

deleted theorem Dfinsupp.sigmaCurry_smul

deleted theorem Dfinsupp.sigmaCurry_zero

deleted def Dfinsupp.sigmaUncurry

deleted theorem Dfinsupp.sigmaUncurry_add

deleted theorem Dfinsupp.sigmaUncurry_apply

deleted theorem Dfinsupp.sigmaUncurry_single

deleted theorem Dfinsupp.sigmaUncurry_smul

deleted theorem Dfinsupp.sigmaUncurry_zero

deleted def Dfinsupp.single

deleted def Dfinsupp.singleAddHom

deleted theorem Dfinsupp.single_add

deleted theorem Dfinsupp.single_add_erase

deleted theorem Dfinsupp.single_apply

deleted theorem Dfinsupp.single_eq_of_ne

deleted theorem Dfinsupp.single_eq_of_sigma_eq

deleted theorem Dfinsupp.single_eq_pi_single

deleted theorem Dfinsupp.single_eq_same

deleted theorem Dfinsupp.single_eq_single_iff

deleted theorem Dfinsupp.single_eq_zero

deleted theorem Dfinsupp.single_injective

deleted theorem Dfinsupp.single_left_injective

deleted theorem Dfinsupp.single_neg

deleted theorem Dfinsupp.single_smul

deleted theorem Dfinsupp.single_sub

deleted theorem Dfinsupp.single_zero

deleted theorem Dfinsupp.smul_apply

deleted theorem Dfinsupp.smul_sum

deleted theorem Dfinsupp.sub_apply

deleted def Dfinsupp.subtypeDomain

deleted def Dfinsupp.subtypeDomainAddMonoidHom

deleted def Dfinsupp.subtypeDomainLinearMap

deleted theorem Dfinsupp.subtypeDomain_add

deleted theorem Dfinsupp.subtypeDomain_apply

deleted theorem Dfinsupp.subtypeDomain_def

deleted theorem Dfinsupp.subtypeDomain_finsupp_sum

deleted theorem Dfinsupp.subtypeDomain_neg

deleted theorem Dfinsupp.subtypeDomain_smul

deleted theorem Dfinsupp.subtypeDomain_sub

deleted theorem Dfinsupp.subtypeDomain_sum

deleted theorem Dfinsupp.subtypeDomain_zero

deleted def Dfinsupp.sumAddHom

deleted theorem Dfinsupp.sumAddHom_add

deleted theorem Dfinsupp.sumAddHom_apply

deleted theorem Dfinsupp.sumAddHom_comm

deleted theorem Dfinsupp.sumAddHom_comp_single

deleted theorem Dfinsupp.sumAddHom_single

deleted theorem Dfinsupp.sumAddHom_singleAddHom

deleted theorem Dfinsupp.sumAddHom_zero

deleted theorem Dfinsupp.sum_apply

deleted theorem Dfinsupp.sum_single

deleted theorem Dfinsupp.sum_sub_index

deleted def Dfinsupp.support

deleted theorem Dfinsupp.support_add

deleted theorem Dfinsupp.support_eq_empty

deleted theorem Dfinsupp.support_erase

deleted theorem Dfinsupp.support_filter

deleted theorem Dfinsupp.support_mapRange

deleted theorem Dfinsupp.support_mk'_subset

deleted theorem Dfinsupp.support_mk_subset

deleted theorem Dfinsupp.support_neg

deleted theorem Dfinsupp.support_single_ne_zero

deleted theorem Dfinsupp.support_single_subset

deleted theorem Dfinsupp.support_smul

deleted theorem Dfinsupp.support_subset_iff

deleted theorem Dfinsupp.support_subtypeDomain

deleted theorem Dfinsupp.support_sum

deleted theorem Dfinsupp.support_update

deleted theorem Dfinsupp.support_update_ne_zero

deleted theorem Dfinsupp.support_zero

deleted theorem Dfinsupp.support_zipWith

deleted theorem Dfinsupp.toFun_eq_coe

deleted def Dfinsupp.update

deleted theorem Dfinsupp.update_eq_erase

deleted theorem Dfinsupp.update_eq_erase_add_single

deleted theorem Dfinsupp.update_eq_single_add_erase

deleted theorem Dfinsupp.update_eq_sub_add_single

deleted theorem Dfinsupp.update_self

deleted theorem Dfinsupp.zero_apply

deleted def Dfinsupp.zipWith

deleted theorem Dfinsupp.zipWith_apply

deleted theorem Dfinsupp.zipWith_def

deleted theorem Dfinsupp.zsmul_apply

deleted structure Dfinsupp

Renamed Mathlib/Data/Dfinsupp/Interval.lean to Mathlib/Data/DFinsupp/Interval.lean

added theorem DFinsupp.Icc_eq

added theorem DFinsupp.card_Icc

added theorem DFinsupp.card_Ico

added theorem DFinsupp.card_Iic

added theorem DFinsupp.card_Iio

added theorem DFinsupp.card_Ioc

added theorem DFinsupp.card_Ioo

added theorem DFinsupp.card_pi

added theorem DFinsupp.mem_pi

added theorem DFinsupp.mem_rangeIcc_apply_iff

added theorem DFinsupp.mem_singleton_apply_iff

added def DFinsupp.pi

added def DFinsupp.rangeIcc

added theorem DFinsupp.rangeIcc_apply

added def DFinsupp.singleton

added theorem DFinsupp.support_rangeIcc_subset

deleted theorem Dfinsupp.Icc_eq

deleted theorem Dfinsupp.card_Icc

deleted theorem Dfinsupp.card_Ico

deleted theorem Dfinsupp.card_Iic

deleted theorem Dfinsupp.card_Iio

deleted theorem Dfinsupp.card_Ioc

deleted theorem Dfinsupp.card_Ioo

deleted theorem Dfinsupp.card_pi

deleted theorem Dfinsupp.mem_pi

deleted theorem Dfinsupp.mem_rangeIcc_apply_iff

deleted theorem Dfinsupp.mem_singleton_apply_iff

deleted def Dfinsupp.pi

deleted def Dfinsupp.rangeIcc

deleted theorem Dfinsupp.rangeIcc_apply

deleted def Dfinsupp.singleton

deleted theorem Dfinsupp.support_rangeIcc_subset

Renamed Mathlib/Data/Dfinsupp/Lex.lean to Mathlib/Data/DFinsupp/Lex.lean

added theorem DFinsupp.lex_def

added theorem DFinsupp.lex_lt_of_lt

added theorem DFinsupp.lex_lt_of_lt_of_preorder

added theorem DFinsupp.lt_of_forall_lt_of_lt

added theorem DFinsupp.toLex_monotone

deleted theorem Dfinsupp.lex_def

deleted theorem Dfinsupp.lex_lt_of_lt

deleted theorem Dfinsupp.lex_lt_of_lt_of_preorder

deleted theorem Dfinsupp.lt_of_forall_lt_of_lt

deleted theorem Dfinsupp.toLex_monotone

Created Mathlib/Data/DFinsupp/Multiset.lean

added def DFinsupp.toMultiset

added theorem DFinsupp.toMultiset_single

added theorem DFinsupp.toMultiset_toDFinsupp

added def Multiset.equivDFinsupp

added def Multiset.toDFinsupp

added theorem Multiset.toDFinsupp_apply

added theorem Multiset.toDFinsupp_le_toDFinsupp

added theorem Multiset.toDFinsupp_replicate

added theorem Multiset.toDFinsupp_singleton

added theorem Multiset.toDFinsupp_support

added theorem Multiset.toDFinsupp_toMultiset

Renamed Mathlib/Data/Dfinsupp/NeLocus.lean to Mathlib/Data/DFinsupp/NeLocus.lean

added theorem DFinsupp.coe_neLocus

added theorem DFinsupp.mapRange_neLocus_eq

added theorem DFinsupp.mem_neLocus

added def DFinsupp.neLocus

added theorem DFinsupp.neLocus_add_left

added theorem DFinsupp.neLocus_add_right

added theorem DFinsupp.neLocus_comm

added theorem DFinsupp.neLocus_eq_empty

added theorem DFinsupp.neLocus_eq_support_sub

added theorem DFinsupp.neLocus_neg

added theorem DFinsupp.neLocus_neg_neg

added theorem DFinsupp.neLocus_self_add_left

added theorem DFinsupp.neLocus_self_add_right

added theorem DFinsupp.neLocus_self_sub_left

added theorem DFinsupp.neLocus_self_sub_right

added theorem DFinsupp.neLocus_sub_left

added theorem DFinsupp.neLocus_sub_right

added theorem DFinsupp.neLocus_zero_left

added theorem DFinsupp.neLocus_zero_right

added theorem DFinsupp.nonempty_neLocus_iff

added theorem DFinsupp.not_mem_neLocus

added theorem DFinsupp.subset_mapRange_neLocus

added theorem DFinsupp.zipWith_neLocus_eq_left

added theorem DFinsupp.zipWith_neLocus_eq_right

deleted theorem Dfinsupp.coe_neLocus

deleted theorem Dfinsupp.mapRange_neLocus_eq

deleted theorem Dfinsupp.mem_neLocus

deleted def Dfinsupp.neLocus

deleted theorem Dfinsupp.neLocus_add_left

deleted theorem Dfinsupp.neLocus_add_right

deleted theorem Dfinsupp.neLocus_comm

deleted theorem Dfinsupp.neLocus_eq_empty

deleted theorem Dfinsupp.neLocus_eq_support_sub

deleted theorem Dfinsupp.neLocus_neg

deleted theorem Dfinsupp.neLocus_neg_neg

deleted theorem Dfinsupp.neLocus_self_add_left

deleted theorem Dfinsupp.neLocus_self_add_right

deleted theorem Dfinsupp.neLocus_self_sub_left

deleted theorem Dfinsupp.neLocus_self_sub_right

deleted theorem Dfinsupp.neLocus_sub_left

deleted theorem Dfinsupp.neLocus_sub_right

deleted theorem Dfinsupp.neLocus_zero_left

deleted theorem Dfinsupp.neLocus_zero_right

deleted theorem Dfinsupp.nonempty_neLocus_iff

deleted theorem Dfinsupp.not_mem_neLocus

deleted theorem Dfinsupp.subset_mapRange_neLocus

deleted theorem Dfinsupp.zipWith_neLocus_eq_left

deleted theorem Dfinsupp.zipWith_neLocus_eq_right

Renamed Mathlib/Data/Dfinsupp/Order.lean to Mathlib/Data/DFinsupp/Order.lean

added theorem DFinsupp.add_eq_zero_iff

added theorem DFinsupp.coeFn_mono

added theorem DFinsupp.coe_tsub

added theorem DFinsupp.inf_apply

added theorem DFinsupp.le_def

added theorem DFinsupp.le_iff'

added theorem DFinsupp.le_iff

added def DFinsupp.orderEmbeddingToFun

added theorem DFinsupp.orderEmbeddingToFun_apply

added theorem DFinsupp.single_le_iff

added theorem DFinsupp.single_tsub

added theorem DFinsupp.subset_support_tsub

added theorem DFinsupp.sup_apply

added theorem DFinsupp.support_inf

added theorem DFinsupp.support_sup

added theorem DFinsupp.support_tsub

added theorem DFinsupp.tsub_apply

deleted theorem Dfinsupp.add_eq_zero_iff

deleted theorem Dfinsupp.coeFn_mono

deleted theorem Dfinsupp.coe_tsub

deleted theorem Dfinsupp.inf_apply

deleted theorem Dfinsupp.le_def

deleted theorem Dfinsupp.le_iff'

deleted theorem Dfinsupp.le_iff

deleted def Dfinsupp.orderEmbeddingToFun

deleted theorem Dfinsupp.orderEmbeddingToFun_apply

deleted theorem Dfinsupp.single_le_iff

deleted theorem Dfinsupp.single_tsub

deleted theorem Dfinsupp.subset_support_tsub

deleted theorem Dfinsupp.sup_apply

deleted theorem Dfinsupp.support_inf

deleted theorem Dfinsupp.support_sup

deleted theorem Dfinsupp.support_tsub

deleted theorem Dfinsupp.tsub_apply

Renamed Mathlib/Data/Dfinsupp/WellFounded.lean to Mathlib/Data/DFinsupp/WellFounded.lean

added theorem DFinsupp.Lex.acc

added theorem DFinsupp.Lex.acc_of_single

added theorem DFinsupp.Lex.acc_of_single_erase

added theorem DFinsupp.Lex.acc_single

added theorem DFinsupp.Lex.acc_zero

added theorem DFinsupp.Lex.wellFounded'

added theorem DFinsupp.Lex.wellFounded

added theorem DFinsupp.Lex.wellFounded_of_finite

added theorem DFinsupp.lex_fibration

deleted theorem Dfinsupp.Lex.acc

deleted theorem Dfinsupp.Lex.acc_of_single

deleted theorem Dfinsupp.Lex.acc_of_single_erase

deleted theorem Dfinsupp.Lex.acc_single

deleted theorem Dfinsupp.Lex.acc_zero

deleted theorem Dfinsupp.Lex.wellFounded'

deleted theorem Dfinsupp.Lex.wellFounded

deleted theorem Dfinsupp.Lex.wellFounded_of_finite

deleted theorem Dfinsupp.lex_fibration

Deleted Mathlib/Data/Dfinsupp/Multiset.lean

deleted def Dfinsupp.toMultiset

deleted theorem Dfinsupp.toMultiset_single

deleted theorem Dfinsupp.toMultiset_toDfinsupp

deleted def Multiset.equivDfinsupp

deleted def Multiset.toDfinsupp

deleted theorem Multiset.toDfinsupp_apply

deleted theorem Multiset.toDfinsupp_le_toDfinsupp

deleted theorem Multiset.toDfinsupp_replicate

deleted theorem Multiset.toDfinsupp_singleton

deleted theorem Multiset.toDfinsupp_support

deleted theorem Multiset.toDfinsupp_toMultiset

Modified Mathlib/Data/Finsupp/Lex.lean

Created Mathlib/Data/Finsupp/ToDFinsupp.lean

added def DFinsupp.toFinsupp

added theorem DFinsupp.toFinsupp_add

added theorem DFinsupp.toFinsupp_coe

added theorem DFinsupp.toFinsupp_neg

added theorem DFinsupp.toFinsupp_single

added theorem DFinsupp.toFinsupp_smul

added theorem DFinsupp.toFinsupp_sub

added theorem DFinsupp.toFinsupp_support

added theorem DFinsupp.toFinsupp_toDFinsupp

added theorem DFinsupp.toFinsupp_zero

added def Finsupp.toDFinsupp

added theorem Finsupp.toDFinsupp_add

added theorem Finsupp.toDFinsupp_coe

added theorem Finsupp.toDFinsupp_neg

added theorem Finsupp.toDFinsupp_single

added theorem Finsupp.toDFinsupp_smul

added theorem Finsupp.toDFinsupp_sub

added theorem Finsupp.toDFinsupp_toFinsupp

added theorem Finsupp.toDFinsupp_zero

added def finsuppAddEquivDFinsupp

added def finsuppEquivDFinsupp

added def finsuppLequivDFinsupp

added theorem finsuppLequivDFinsupp_apply_apply

added theorem finsuppLequivDFinsupp_symm_apply

added def sigmaFinsuppAddEquivDFinsupp

added def sigmaFinsuppEquivDFinsupp

added theorem sigmaFinsuppEquivDFinsupp_add

added theorem sigmaFinsuppEquivDFinsupp_apply

added theorem sigmaFinsuppEquivDFinsupp_single

added theorem sigmaFinsuppEquivDFinsupp_smul

added theorem sigmaFinsuppEquivDFinsupp_support

added theorem sigmaFinsuppEquivDFinsupp_symm_apply

added def sigmaFinsuppLequivDFinsupp

added theorem toDFinsupp_support

Deleted Mathlib/Data/Finsupp/ToDfinsupp.lean

deleted def Dfinsupp.toFinsupp

deleted theorem Dfinsupp.toFinsupp_add

deleted theorem Dfinsupp.toFinsupp_coe

deleted theorem Dfinsupp.toFinsupp_neg

deleted theorem Dfinsupp.toFinsupp_single

deleted theorem Dfinsupp.toFinsupp_smul

deleted theorem Dfinsupp.toFinsupp_sub

deleted theorem Dfinsupp.toFinsupp_support

deleted theorem Dfinsupp.toFinsupp_toDfinsupp

deleted theorem Dfinsupp.toFinsupp_zero

deleted def Finsupp.toDfinsupp

deleted theorem Finsupp.toDfinsupp_add

deleted theorem Finsupp.toDfinsupp_coe

deleted theorem Finsupp.toDfinsupp_neg

deleted theorem Finsupp.toDfinsupp_single

deleted theorem Finsupp.toDfinsupp_smul

deleted theorem Finsupp.toDfinsupp_sub

deleted theorem Finsupp.toDfinsupp_toFinsupp

deleted theorem Finsupp.toDfinsupp_zero

deleted def finsuppAddEquivDfinsupp

deleted def finsuppEquivDfinsupp

deleted def finsuppLequivDfinsupp

deleted theorem finsuppLequivDfinsupp_apply_apply

deleted theorem finsuppLequivDfinsupp_symm_apply

deleted def sigmaFinsuppAddEquivDfinsupp

deleted def sigmaFinsuppEquivDfinsupp

deleted theorem sigmaFinsuppEquivDfinsupp_add

deleted theorem sigmaFinsuppEquivDfinsupp_apply

deleted theorem sigmaFinsuppEquivDfinsupp_single

deleted theorem sigmaFinsuppEquivDfinsupp_smul

deleted theorem sigmaFinsuppEquivDfinsupp_support

deleted theorem sigmaFinsuppEquivDfinsupp_symm_apply

deleted def sigmaFinsuppLequivDfinsupp

deleted theorem toDfinsupp_support

Modified Mathlib/Data/Finsupp/WellFounded.lean

Modified Mathlib/Data/Multiset/Interval.lean

Modified Mathlib/GroupTheory/FiniteAbelian.lean

Modified Mathlib/LinearAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/CliffordAlgebra/Grading.lean

Renamed Mathlib/LinearAlgebra/Dfinsupp.lean to Mathlib/LinearAlgebra/DFinsupp.lean

added theorem DFinsupp.coprodMap_apply

added theorem DFinsupp.coprodMap_apply_single

added def DFinsupp.lapply

added theorem DFinsupp.lapply_apply

added theorem DFinsupp.lhom_ext'

added theorem DFinsupp.lhom_ext

added def DFinsupp.lmk

added theorem DFinsupp.lmk_apply

added def DFinsupp.lsingle

added theorem DFinsupp.lsingle_apply

added def DFinsupp.lsum

added theorem DFinsupp.lsum_single

added def DFinsupp.mapRange.linearEquiv

added theorem DFinsupp.mapRange.linearEquiv_refl

added theorem DFinsupp.mapRange.linearEquiv_symm

added theorem DFinsupp.mapRange.linearEquiv_trans

added def DFinsupp.mapRange.linearMap

added theorem DFinsupp.mapRange.linearMap_comp

added theorem DFinsupp.mapRange.linearMap_id

added theorem DFinsupp.mapRange_smul

added theorem DFinsupp.sum_mapRange_index.linearMap

deleted theorem Dfinsupp.coprodMap_apply

deleted theorem Dfinsupp.coprodMap_apply_single

deleted def Dfinsupp.lapply

deleted theorem Dfinsupp.lapply_apply

deleted theorem Dfinsupp.lhom_ext'

deleted theorem Dfinsupp.lhom_ext

deleted def Dfinsupp.lmk

deleted theorem Dfinsupp.lmk_apply

deleted def Dfinsupp.lsingle

deleted theorem Dfinsupp.lsingle_apply

deleted def Dfinsupp.lsum

deleted theorem Dfinsupp.lsum_single

deleted def Dfinsupp.mapRange.linearEquiv

deleted theorem Dfinsupp.mapRange.linearEquiv_refl

deleted theorem Dfinsupp.mapRange.linearEquiv_symm

deleted theorem Dfinsupp.mapRange.linearEquiv_trans

deleted def Dfinsupp.mapRange.linearMap

deleted theorem Dfinsupp.mapRange.linearMap_comp

deleted theorem Dfinsupp.mapRange.linearMap_id

deleted theorem Dfinsupp.mapRange_smul

deleted theorem Dfinsupp.sum_mapRange_index.linearMap

Modified Mathlib/LinearAlgebra/Dimension.lean

Modified Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean

Modified Mathlib/LinearAlgebra/ExteriorAlgebra/Grading.lean

Modified Mathlib/LinearAlgebra/FreeModule/Basic.lean

Modified Mathlib/LinearAlgebra/FreeModule/Rank.lean

Modified Mathlib/RingTheory/Coprime/Ideal.lean

Modified Mathlib/RingTheory/GradedAlgebra/Basic.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousIdeal.lean

Modified Mathlib/Testing/SlimCheck/Functions.lean

Modified test/slim_check.lean