Commit 2025-04-09 08:09 79096ed0

View on Github →

refactor: correct names for (D)Finsupp.sum lemmas (#23741) The naming guide advocates finsuppSum not finsupp_sum as we wrote in Lean 3.

Estimated changes

Modified Mathlib/Algebra/BigOperators/Associated.lean

added theorem Prime.dvd_finsuppProd_iff

deleted theorem Prime.dvd_finsupp_prod_iff

added theorem Prime.not_dvd_finsuppProd

deleted theorem Prime.not_dvd_finsupp_prod

Modified Mathlib/Algebra/BigOperators/Finsupp/Basic.lean

added theorem MonoidHom.coe_finsuppProd

deleted theorem MonoidHom.coe_finsupp_prod

added theorem MonoidHom.finsuppProd_apply

deleted theorem MonoidHom.finsupp_prod_apply

added theorem SubmonoidClass.finsuppProd_mem

deleted theorem SubmonoidClass.finsupp_prod_mem

added theorem map_finsuppProd

deleted theorem map_finsupp_prod

Modified Mathlib/Algebra/Category/ModuleCat/Free.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

added theorem DirectSum.coeAddMonoidHom_eq_dfinsuppSum

deleted theorem DirectSum.coeAddMonoidHom_eq_dfinsupp_sum

Modified Mathlib/Algebra/DirectSum/Internal.lean

added theorem DirectSum.coe_mul_apply_eq_dfinsuppSum

deleted theorem DirectSum.coe_mul_apply_eq_dfinsupp_sum

Modified Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.coeLinearMap_eq_dfinsuppSum

deleted theorem DirectSum.coeLinearMap_eq_dfinsupp_sum

Modified Mathlib/Algebra/DirectSum/Ring.lean

added theorem DirectSum.mul_eq_dfinsuppSum

deleted theorem DirectSum.mul_eq_dfinsupp_sum

Modified Mathlib/Algebra/Module/Projective.lean

Modified Mathlib/Algebra/MonoidAlgebra/Defs.lean

Modified Mathlib/Algebra/MvPolynomial/Equiv.lean

Modified Mathlib/Algebra/Order/Antidiag/Finsupp.lean

Modified Mathlib/Analysis/InnerProductSpace/l2Space.lean

Modified Mathlib/Analysis/RCLike/Basic.lean

added theorem RCLike.ofReal_finsuppProd

deleted theorem RCLike.ofReal_finsupp_prod

Modified Mathlib/Analysis/SpecialFunctions/Log/Basic.lean

Modified Mathlib/Combinatorics/Nullstellensatz.lean

Modified Mathlib/Data/DFinsupp/BigOperators.lean

added theorem AddEquiv.map_dfinsuppSumAddHom

deleted theorem AddEquiv.map_dfinsupp_sumAddHom

added theorem AddMonoidHom.coe_dfinsuppSumAddHom

deleted theorem AddMonoidHom.coe_dfinsupp_sumAddHom

added theorem AddMonoidHom.dfinsuppSumAddHom_apply

deleted theorem AddMonoidHom.dfinsupp_sumAddHom_apply

added theorem AddMonoidHom.map_dfinsuppSumAddHom

deleted theorem AddMonoidHom.map_dfinsupp_sumAddHom

added theorem MonoidHom.coe_dfinsuppProd

deleted theorem MonoidHom.coe_dfinsupp_prod

added theorem MonoidHom.dfinsuppProd_apply

deleted theorem MonoidHom.dfinsupp_prod_apply

added theorem RingHom.map_dfinsuppSumAddHom

deleted theorem RingHom.map_dfinsupp_sumAddHom

added theorem map_dfinsuppProd

deleted theorem map_dfinsupp_prod

Modified Mathlib/Data/DFinsupp/Submonoid.lean

added theorem AddSubmonoid.bsupr_eq_mrange_dfinsuppSumAddHom

deleted theorem AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom

added theorem AddSubmonoid.iSup_eq_mrange_dfinsuppSumAddHom

deleted theorem AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom

added theorem dfinsuppProd_mem

added theorem dfinsuppSumAddHom_mem

deleted theorem dfinsupp_prod_mem

deleted theorem dfinsupp_sumAddHom_mem

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Int.cast_finsuppProd

deleted theorem Int.cast_finsupp_prod

added theorem Nat.cast_finsuppProd

deleted theorem Nat.cast_finsupp_prod

added theorem Rat.cast_finsuppProd

deleted theorem Rat.cast_finsupp_prod

Modified Mathlib/Data/Finsupp/Multiset.lean

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

added theorem LinearEquiv.map_dfinsuppSumAddHom

deleted theorem LinearEquiv.map_dfinsupp_sumAddHom

added theorem LinearMap.coe_dfinsuppSum

deleted theorem LinearMap.coe_dfinsupp_sum

added theorem LinearMap.dfinsuppSum_apply

deleted theorem LinearMap.dfinsupp_sum_apply

added theorem LinearMap.map_dfinsuppSumAddHom

deleted theorem LinearMap.map_dfinsupp_sumAddHom

added theorem Submodule.dfinsuppSumAddHom_mem

added theorem Submodule.dfinsuppSum_mem

deleted theorem Submodule.dfinsupp_sumAddHom_mem

deleted theorem Submodule.dfinsupp_sum_mem

added theorem iSupIndep.dfinsuppSumAddHom_injective

deleted theorem iSupIndep.dfinsupp_sumAddHom_injective

added theorem iSupIndep_iff_dfinsuppSumAddHom_injective

deleted theorem iSupIndep_iff_dfinsupp_sumAddHom_injective

added theorem iSupIndep_of_dfinsuppSumAddHom_injective'

added theorem iSupIndep_of_dfinsuppSumAddHom_injective

deleted theorem iSupIndep_of_dfinsupp_sumAddHom_injective'

deleted theorem iSupIndep_of_dfinsupp_sumAddHom_injective

Modified Mathlib/LinearAlgebra/Dimension/Constructions.lean

Modified Mathlib/LinearAlgebra/Dual/Basis.lean

Modified Mathlib/LinearAlgebra/Eigenspace/Triangularizable.lean

Modified Mathlib/LinearAlgebra/Finsupp/LSum.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

added theorem FractionalIdeal.count_finsuppProd

deleted theorem FractionalIdeal.count_finsupp_prod

Modified Mathlib/RingTheory/Generators.lean

Modified Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean

added theorem MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum

deleted theorem MvPolynomial.DirectSum.coeLinearMap_eq_dfinsupp_sum

Modified Mathlib/RingTheory/MvPowerSeries/Basic.lean

Modified Mathlib/RingTheory/Presentation.lean

Modified Mathlib/RingTheory/Unramified/Finite.lean

Modified Mathlib/Topology/Category/Profinite/Nobeling.lean

added theorem Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval

deleted theorem Profinite.NobelingProof.GoodProducts.finsupp_sum_mem_span_eval

Modified scripts/nolints_prime_decls.txt