Commit 2026-04-26 16:26 67707479

View on Github →

chore: camel-case finset_sum in lemma names (#37793) and finset_prod too. Done with grep with the bogus replacements reverted by hand.

Estimated changes

Modified Mathlib/Algebra/Algebra/Operations.lean

Modified Mathlib/Algebra/Algebra/Subalgebra/Operations.lean

added theorem Subalgebra.mem_of_finsetSum_eq_one_of_pow_smul_mem

deleted theorem Subalgebra.mem_of_finset_sum_eq_one_of_pow_smul_mem

Modified Mathlib/Algebra/BigOperators/Associated.lean

added theorem Associates.finsetProd_mk

deleted theorem Associates.finset_prod_mk

added theorem Prime.dvd_finsetProd_iff

deleted theorem Prime.dvd_finset_prod_iff

added theorem Prime.not_dvd_finsetProd

deleted theorem Prime.not_dvd_finset_prod

Modified Mathlib/Algebra/BigOperators/Fin.lean

added theorem List.alternatingProd_eq_finsetProd

deleted theorem List.alternatingProd_eq_finset_prod

Modified Mathlib/Algebra/BigOperators/Finprod.lean

added theorem finprod_eq_finsetProd_of_mulSupport_subset

deleted theorem finprod_eq_finset_prod_of_mulSupport_subset

added theorem map_finsetProd

deleted theorem map_finset_prod

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

added theorem Finsupp.coe_finsetSum

deleted theorem Finsupp.coe_finset_sum

added theorem Finsupp.finsetSum_apply

deleted theorem Finsupp.finset_sum_apply

added theorem Finsupp.prod_finsetSum_index

deleted theorem Finsupp.prod_finset_sum_index

added theorem Finsupp.single_finsetSum

deleted theorem Finsupp.single_finset_sum

added theorem Finsupp.support_finsetSum

deleted theorem Finsupp.support_finset_sum

Modified Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean

added theorem Multiset.disjoint_finsetSum_left

added theorem Multiset.disjoint_finsetSum_right

deleted theorem Multiset.disjoint_finset_sum_left

deleted theorem Multiset.disjoint_finset_sum_right

Modified Mathlib/Algebra/BigOperators/Group/Finset/Lemmas.lean

added theorem MonoidHom.coe_finsetProd

deleted theorem MonoidHom.coe_finset_prod

added theorem MonoidHom.finsetProd_apply

deleted theorem MonoidHom.finset_prod_apply

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/DirectSum/Basic.lean

Modified Mathlib/Algebra/DirectSum/Idempotents.lean

Modified Mathlib/Algebra/DirectSum/Internal.lean

Modified Mathlib/Algebra/Group/EvenFunction.lean

added theorem Function.Odd.finsetSum_eq_zero

deleted theorem Function.Odd.finset_sum_eq_zero

Modified Mathlib/Algebra/Group/ForwardDiff.lean

added theorem fwdDiff_finsetSum

deleted theorem fwdDiff_finset_sum

added theorem fwdDiff_iter_finsetSum

deleted theorem fwdDiff_iter_finset_sum

Modified Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean

added theorem Set.finsetProd_mem_finsetProd

added theorem Set.finsetProd_singleton

added theorem Set.finsetProd_subset_finsetProd

deleted theorem Set.finset_prod_mem_finset_prod

deleted theorem Set.finset_prod_singleton

deleted theorem Set.finset_prod_subset_finset_prod

added theorem Set.image_finsetProd

added theorem Set.image_finsetProd_pi

deleted theorem Set.image_finset_prod

deleted theorem Set.image_finset_prod_pi

added theorem Set.mem_finsetProd

deleted theorem Set.mem_finset_prod

Modified Mathlib/Algebra/Group/Subgroup/Finite.lean

added theorem Subgroup.val_finsetProd

deleted theorem Subgroup.val_finset_prod

Modified Mathlib/Algebra/Group/Submonoid/BigOperators.lean

added theorem Submonoid.coe_finsetProd

deleted theorem Submonoid.coe_finset_prod

added theorem SubmonoidClass.coe_finsetProd

deleted theorem SubmonoidClass.coe_finset_prod

Modified Mathlib/Algebra/Lie/Loop.lean

Modified Mathlib/Algebra/LinearRecurrence.lean

Modified Mathlib/Algebra/Module/LocalizedModule/Int.lean

Modified Mathlib/Algebra/Module/Submodule/Finsupp.lean

Modified Mathlib/Algebra/Module/Submodule/LinearMap.lean

Modified Mathlib/Algebra/Module/Torsion/Basic.lean

Modified Mathlib/Algebra/Module/Torsion/PrimaryComponent.lean

Modified Mathlib/Algebra/MonoidAlgebra/Degree.lean

added theorem AddMonoidAlgebra.le_inf_support_finsetProd

deleted theorem AddMonoidAlgebra.le_inf_support_finset_prod

added theorem AddMonoidAlgebra.sup_support_finsetProd_le

deleted theorem AddMonoidAlgebra.sup_support_finset_prod_le

Modified Mathlib/Algebra/MonoidAlgebra/MapDomain.lean

Modified Mathlib/Algebra/MvPolynomial/Basic.lean

Modified Mathlib/Algebra/MvPolynomial/Degrees.lean

added theorem MvPolynomial.totalDegree_finsetProd

added theorem MvPolynomial.totalDegree_finsetSum

deleted theorem MvPolynomial.totalDegree_finset_prod

deleted theorem MvPolynomial.totalDegree_finset_sum

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

Modified Mathlib/Algebra/Order/BigOperators/Group/Finset.lean

added theorem Multiset.finsetSum_eq_sup_iff_disjoint

deleted theorem Multiset.finset_sum_eq_sup_iff_disjoint

Modified Mathlib/Algebra/Polynomial/BigOperators.lean

added theorem Polynomial.natDegree_finsetProd_X_sub_C_eq_card

deleted theorem Polynomial.natDegree_finset_prod_X_sub_C_eq_card

Modified Mathlib/Algebra/Polynomial/Bivariate.lean

added theorem Polynomial.evalEval_finsetSum

deleted theorem Polynomial.evalEval_finset_sum

Modified Mathlib/Algebra/Polynomial/Coeff.lean

added theorem Polynomial.finsetSum_coeff

deleted theorem Polynomial.finset_sum_coeff

Modified Mathlib/Algebra/Polynomial/EraseLead.lean

Modified Mathlib/Algebra/Polynomial/Eval/Defs.lean

added theorem Polynomial.eval_finsetSum

deleted theorem Polynomial.eval_finset_sum

added theorem Polynomial.eval₂_finsetProd

added theorem Polynomial.eval₂_finsetSum

deleted theorem Polynomial.eval₂_finset_prod

deleted theorem Polynomial.eval₂_finset_sum

Modified Mathlib/Algebra/Polynomial/Eval/Degree.lean

Modified Mathlib/Algebra/Polynomial/Expand.lean

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/Polynomial/HasseDeriv.lean

Modified Mathlib/Algebra/Polynomial/Lifts.lean

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

Modified Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Proper.lean

Modified Mathlib/AlgebraicGeometry/SpreadingOut.lean

Modified Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean

Modified Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

Modified Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean

Modified Mathlib/Analysis/Calculus/Deriv/Mul.lean

added theorem Differentiable.finsetProd

deleted theorem Differentiable.finset_prod

added theorem Differentiable.fun_finsetProd

deleted theorem Differentiable.fun_finset_prod

added theorem DifferentiableAt.finsetProd

deleted theorem DifferentiableAt.finset_prod

added theorem DifferentiableAt.fun_finsetProd

deleted theorem DifferentiableAt.fun_finset_prod

added theorem DifferentiableOn.finsetProd

deleted theorem DifferentiableOn.finset_prod

added theorem DifferentiableOn.fun_finsetProd

deleted theorem DifferentiableOn.fun_finset_prod

added theorem DifferentiableWithinAt.finsetProd

deleted theorem DifferentiableWithinAt.finset_prod

added theorem DifferentiableWithinAt.fun_finsetProd

deleted theorem DifferentiableWithinAt.fun_finset_prod

added theorem HasDerivAt.finsetProd

deleted theorem HasDerivAt.finset_prod

added theorem HasDerivAt.fun_finsetProd

deleted theorem HasDerivAt.fun_finset_prod

added theorem HasDerivWithinAt.finsetProd

deleted theorem HasDerivWithinAt.finset_prod

added theorem HasDerivWithinAt.fun_finsetProd

deleted theorem HasDerivWithinAt.fun_finset_prod

added theorem HasStrictDerivAt.finsetProd

deleted theorem HasStrictDerivAt.finset_prod

added theorem HasStrictDerivAt.fun_finsetProd

deleted theorem HasStrictDerivAt.fun_finset_prod

added theorem derivWithin_finsetProd

deleted theorem derivWithin_finset_prod

added theorem derivWithin_fun_finsetProd

deleted theorem derivWithin_fun_finset_prod

added theorem deriv_finsetProd

deleted theorem deriv_finset_prod

added theorem deriv_fun_finsetProd

deleted theorem deriv_fun_finset_prod

Modified Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

Modified Mathlib/Analysis/Calculus/FDeriv/Mul.lean

added theorem HasFDerivAt.finsetProd

deleted theorem HasFDerivAt.finset_prod

added theorem HasFDerivWithinAt.finsetProd

deleted theorem HasFDerivWithinAt.finset_prod

added theorem HasStrictFDerivAt.finsetProd

deleted theorem HasStrictFDerivAt.finset_prod

added theorem fderivWithin_finsetProd

deleted theorem fderivWithin_finset_prod

added theorem fderiv_finsetProd

deleted theorem fderiv_finset_prod

added theorem hasFDerivAt_finsetProd

deleted theorem hasFDerivAt_finset_prod

added theorem hasStrictFDerivAt_finsetProd

deleted theorem hasStrictFDerivAt_finset_prod

Modified Mathlib/Analysis/Calculus/LogDeriv.lean

Modified Mathlib/Analysis/Calculus/Rademacher.lean

Modified Mathlib/Analysis/Calculus/Taylor.lean

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean

Modified Mathlib/Analysis/Fourier/AddCircle.lean

Modified Mathlib/Analysis/Fourier/FourierTransformDeriv.lean

Modified Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

Modified Mathlib/Analysis/MeanInequalities.lean

Modified Mathlib/Analysis/MeanInequalitiesPow.lean

Modified Mathlib/Analysis/Normed/Field/Approximation.lean

Modified Mathlib/Analysis/Normed/Group/FunctionSeries.lean

Modified Mathlib/Analysis/Normed/Group/Tannery.lean

Modified Mathlib/Analysis/Normed/Group/Ultra.lean

added theorem IsUltrametricDist.exists_norm_finsetProd_le

added theorem IsUltrametricDist.exists_norm_finsetProd_le_of_nonempty

deleted theorem IsUltrametricDist.exists_norm_finset_prod_le

deleted theorem IsUltrametricDist.exists_norm_finset_prod_le_of_nonempty

Modified Mathlib/Analysis/Normed/Lp/lpSpace.lean

added theorem Memℓp.finsetSum

deleted theorem Memℓp.finset_sum

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Analysis/Normed/Ring/InfiniteProd.lean

Modified Mathlib/Analysis/Normed/Ring/InfiniteSum.lean

Modified Mathlib/Analysis/Normed/Unbundled/FiniteExtension.lean

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

added theorem Multipliable.eventually_bounded_finsetProd

deleted theorem Multipliable.eventually_bounded_finset_prod

added theorem summable_finsetProd_of_summable_nonneg

added theorem summable_finsetProd_of_summable_norm

deleted theorem summable_finset_prod_of_summable_nonneg

deleted theorem summable_finset_prod_of_summable_norm

Modified Mathlib/Analysis/SpecialFunctions/Pochhammer.lean

Modified Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean

added theorem NNReal.finsetProd_rpow

deleted theorem NNReal.finset_prod_rpow

added theorem Real.finsetProd_rpow

deleted theorem Real.finset_prod_rpow

Modified Mathlib/Analysis/SpecialFunctions/Pow/Real.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/ChebyshevGauss.lean

Modified Mathlib/Analysis/SpecialFunctions/Trigonometric/Chebyshev/RootsExtrema.lean

Modified Mathlib/Analysis/SpecificLimits/Normed.lean

Modified Mathlib/Combinatorics/Hindman.lean

added theorem Hindman.FP.finsetProd

deleted theorem Hindman.FP.finset_prod

Modified Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean

Modified Mathlib/Computability/AkraBazzi/SumTransform.lean

Modified Mathlib/Data/DFinsupp/BigOperators.lean

added theorem DFinsupp.coe_finsetSum

deleted theorem DFinsupp.coe_finset_sum

added theorem DFinsupp.finsetSum_apply

deleted theorem DFinsupp.finset_sum_apply

added theorem DFinsupp.prod_finsetSum_index

deleted theorem DFinsupp.prod_finset_sum_index

Modified Mathlib/Data/ENNReal/BigOperators.lean

added theorem ENNReal.coe_finsetProd

added theorem ENNReal.coe_finsetSum

deleted theorem ENNReal.coe_finset_prod

deleted theorem ENNReal.coe_finset_sum

Modified Mathlib/Data/Finsupp/Basic.lean

added theorem Finsupp.mapDomain_finsetSum

deleted theorem Finsupp.mapDomain_finset_sum

added theorem Finsupp.mapRange_finsetSum

deleted theorem Finsupp.mapRange_finset_sum

added theorem Finsupp.mem_support_finsetSum

deleted theorem Finsupp.mem_support_finset_sum

Modified Mathlib/Data/Nat/Choose/Lucas.lean

Modified Mathlib/Data/Nat/Factorization/Basic.lean

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/Data/ZMod/Units.lean

Modified Mathlib/FieldTheory/ChevalleyWarning.lean

Modified Mathlib/FieldTheory/IntermediateField/Basic.lean

Modified Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean

Modified Mathlib/Geometry/Manifold/Algebra/Monoid.lean

added theorem contMDiffAt_finsetProd'

added theorem contMDiffAt_finsetProd

deleted theorem contMDiffAt_finset_prod'

deleted theorem contMDiffAt_finset_prod

added theorem contMDiffOn_finsetProd'

added theorem contMDiffOn_finsetProd

deleted theorem contMDiffOn_finset_prod'

deleted theorem contMDiffOn_finset_prod

added theorem contMDiffWithinAt_finsetProd'

added theorem contMDiffWithinAt_finsetProd

deleted theorem contMDiffWithinAt_finset_prod'

deleted theorem contMDiffWithinAt_finset_prod

added theorem contMDiff_finsetProd'

added theorem contMDiff_finsetProd

deleted theorem contMDiff_finset_prod'

deleted theorem contMDiff_finset_prod

Modified Mathlib/GroupTheory/Congruence/BigOperators.lean

Modified Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean

Modified Mathlib/LinearAlgebra/DFinsupp.lean

added theorem iSupIndep_iff_finsetSum_eq_imp_eq

added theorem iSupIndep_iff_finsetSum_eq_zero_imp_eq_zero

deleted theorem iSupIndep_iff_finset_sum_eq_imp_eq

deleted theorem iSupIndep_iff_finset_sum_eq_zero_imp_eq_zero

Modified Mathlib/LinearAlgebra/Dimension/LinearMap.lean

added theorem LinearMap.rank_finsetSum_le

deleted theorem LinearMap.rank_finset_sum_le

Modified Mathlib/LinearAlgebra/Finsupp/Pi.lean

Modified Mathlib/LinearAlgebra/Lagrange.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/Matrix/Ideal.lean

Modified Mathlib/LinearAlgebra/Matrix/Polynomial.lean

Modified Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

Modified Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

added theorem MeasureTheory.condExp_finsetSum

deleted theorem MeasureTheory.condExp_finset_sum

Modified Mathlib/MeasureTheory/Function/ConditionalLExpectation.lean

added theorem MeasureTheory.condLExp_finsetSum

deleted theorem MeasureTheory.condLExp_finset_sum

Modified Mathlib/MeasureTheory/Function/Intersectivity.lean

Modified Mathlib/MeasureTheory/Function/L1Space/Integrable.lean

added theorem MeasureTheory.integrable_finsetSum'

added theorem MeasureTheory.integrable_finsetSum

added theorem MeasureTheory.integrable_finsetSum_measure

deleted theorem MeasureTheory.integrable_finset_sum'

deleted theorem MeasureTheory.integrable_finset_sum

deleted theorem MeasureTheory.integrable_finset_sum_measure

Modified Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

added theorem MeasureTheory.locallyIntegrable_finsetSum'

added theorem MeasureTheory.locallyIntegrable_finsetSum

deleted theorem MeasureTheory.locallyIntegrable_finset_sum'

deleted theorem MeasureTheory.locallyIntegrable_finset_sum

Modified Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean

added theorem MeasureTheory.memLp_finsetSum'

added theorem MeasureTheory.memLp_finsetSum

deleted theorem MeasureTheory.memLp_finset_sum'

deleted theorem MeasureTheory.memLp_finset_sum

Modified Mathlib/MeasureTheory/Function/SimpleFunc.lean

added theorem MeasureTheory.SimpleFunc.lintegral_finsetSum

deleted theorem MeasureTheory.SimpleFunc.lintegral_finset_sum

Modified Mathlib/MeasureTheory/Integral/Bochner/Basic.lean

added theorem MeasureTheory.integral_finsetSum

added theorem MeasureTheory.integral_finsetSum_measure

deleted theorem MeasureTheory.integral_finset_sum

deleted theorem MeasureTheory.integral_finset_sum_measure

Modified Mathlib/MeasureTheory/Integral/Bochner/Set.lean

Modified Mathlib/MeasureTheory/Integral/Bochner/SumMeasure.lean

Modified Mathlib/MeasureTheory/Integral/CircleAverage.lean

Modified Mathlib/MeasureTheory/Integral/CircleIntegral.lean

Modified Mathlib/MeasureTheory/Integral/DivergenceTheorem.lean

Modified Mathlib/MeasureTheory/Integral/DominatedConvergence.lean

Modified Mathlib/MeasureTheory/Integral/IntervalIntegral/Basic.lean

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Add.lean

added theorem MeasureTheory.lintegral_finsetSum'

added theorem MeasureTheory.lintegral_finsetSum

deleted theorem MeasureTheory.lintegral_finset_sum'

deleted theorem MeasureTheory.lintegral_finset_sum

Modified Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

added theorem MeasureTheory.lintegral_finsetSum_measure

deleted theorem MeasureTheory.lintegral_finset_sum_measure

Modified Mathlib/MeasureTheory/Integral/SetToL1.lean

added theorem MeasureTheory.setToFun_finsetSum'

added theorem MeasureTheory.setToFun_finsetSum

deleted theorem MeasureTheory.setToFun_finset_sum'

deleted theorem MeasureTheory.setToFun_finset_sum

Modified Mathlib/MeasureTheory/Measure/CharacteristicFunction/Basic.lean

Modified Mathlib/MeasureTheory/Measure/Dirac.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasure.lean

Modified Mathlib/MeasureTheory/Measure/FiniteMeasurePi.lean

Modified Mathlib/MeasureTheory/Measure/GiryMonad.lean

Modified Mathlib/MeasureTheory/Measure/Haar/OfBasis.lean

Modified Mathlib/MeasureTheory/Measure/HasOuterApproxClosedProd.lean

Modified Mathlib/MeasureTheory/Measure/Hausdorff.lean

Modified Mathlib/MeasureTheory/Measure/LevyConvergence.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

added theorem MeasureTheory.Measure.coe_finsetSum

deleted theorem MeasureTheory.Measure.coe_finset_sum

added theorem MeasureTheory.Measure.finsetSum_apply

deleted theorem MeasureTheory.Measure.finset_sum_apply

Modified Mathlib/MeasureTheory/Measure/Portmanteau.lean

Modified Mathlib/MeasureTheory/Measure/Prokhorov.lean

Modified Mathlib/MeasureTheory/Measure/Regular.lean

Modified Mathlib/MeasureTheory/Measure/TightNormed.lean

Modified Mathlib/MeasureTheory/SpecificCodomains/Pi.lean

Modified Mathlib/ModelTheory/Algebra/Field/IsAlgClosed.lean

Modified Mathlib/ModelTheory/Arithmetic/Presburger/Semilinear/Basic.lean

Modified Mathlib/NumberTheory/ArithmeticFunction/Carmichael.lean

added theorem ArithmeticFunction.carmichael_finsetProd

deleted theorem ArithmeticFunction.carmichael_finset_prod

Modified Mathlib/NumberTheory/BernoulliPolynomials.lean

Modified Mathlib/NumberTheory/LSeries/DirichletContinuation.lean

Modified Mathlib/NumberTheory/LSeries/PrimesInAP.lean

Modified Mathlib/NumberTheory/LSeries/ZMod.lean

Modified Mathlib/NumberTheory/ModularForms/DedekindEta.lean

Modified Mathlib/NumberTheory/ModularForms/NormTrace.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

Modified Mathlib/NumberTheory/NumberField/CanonicalEmbedding/NormLeOne.lean

Modified Mathlib/NumberTheory/NumberField/Ideal/Asymptotics.lean

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/Basic.lean

Modified Mathlib/NumberTheory/Primorial.lean

Modified Mathlib/NumberTheory/ZetaValues.lean

Modified Mathlib/Order/Filter/AtTopBot/BigOperators.lean

added theorem Filter.map_atTop_finsetProd_le_of_prod_eq

deleted theorem Filter.map_atTop_finset_prod_le_of_prod_eq

added theorem Function.Injective.map_atTop_finsetProd_eq

deleted theorem Function.Injective.map_atTop_finset_prod_eq

Modified Mathlib/Order/Filter/AtTopBot/Prod.lean

added theorem Filter.tendsto_finsetProd_atTop

deleted theorem Filter.tendsto_finset_prod_atTop

Modified Mathlib/Probability/CentralLimitTheorem.lean

Modified Mathlib/Probability/ConditionalProbability.lean

Modified Mathlib/Probability/Distributions/Gaussian/HasGaussianLaw/Independence.lean

Modified Mathlib/Probability/Distributions/Gaussian/Multivariate.lean

Modified Mathlib/Probability/Independence/Basic.lean

added theorem ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem

added theorem ProbabilityTheory.iIndepFun.indepFun_finsetProd_of_notMem₀

deleted theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem

deleted theorem ProbabilityTheory.iIndepFun.indepFun_finset_prod_of_notMem₀

Modified Mathlib/Probability/Independence/CharacteristicFunction.lean

added theorem ProbabilityTheory.iIndepFun.charFunDual_map_finsetSum_eq_prod

deleted theorem ProbabilityTheory.iIndepFun.charFunDual_map_finset_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFunDual_map_fun_finsetSum_eq_prod

deleted theorem ProbabilityTheory.iIndepFun.charFunDual_map_fun_finset_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFun_map_finsetSum_eq_prod

deleted theorem ProbabilityTheory.iIndepFun.charFun_map_finset_sum_eq_prod

added theorem ProbabilityTheory.iIndepFun.charFun_map_fun_finsetSum_eq_prod

deleted theorem ProbabilityTheory.iIndepFun.charFun_map_fun_finset_sum_eq_prod

Modified Mathlib/Probability/Independence/Conditional.lean

added theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finsetProd_of_notMem

deleted theorem ProbabilityTheory.iCondIndepFun.condIndepFun_finset_prod_of_notMem

Modified Mathlib/Probability/Independence/Integration.lean

Modified Mathlib/Probability/Independence/Kernel/IndepFun.lean

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem

added theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem₀

deleted theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem

deleted theorem ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem₀

Modified Mathlib/Probability/Kernel/Defs.lean

added theorem ProbabilityTheory.Kernel.IsSFiniteKernel.finsetSum

deleted theorem ProbabilityTheory.Kernel.IsSFiniteKernel.finset_sum

added theorem ProbabilityTheory.Kernel.coe_finsetSum

deleted theorem ProbabilityTheory.Kernel.coe_finset_sum

added theorem ProbabilityTheory.Kernel.finsetSum_apply'

added theorem ProbabilityTheory.Kernel.finsetSum_apply

deleted theorem ProbabilityTheory.Kernel.finset_sum_apply'

deleted theorem ProbabilityTheory.Kernel.finset_sum_apply

Modified Mathlib/Probability/Kernel/WithDensity.lean

Modified Mathlib/Probability/Martingale/Basic.lean

Modified Mathlib/Probability/Martingale/BorelCantelli.lean

Modified Mathlib/Probability/Martingale/Centering.lean

Modified Mathlib/Probability/Martingale/OptionalStopping.lean

Modified Mathlib/Probability/Martingale/Upcrossing.lean

Modified Mathlib/Probability/Moments/Basic.lean

Modified Mathlib/Probability/Moments/Covariance.lean

Modified Mathlib/Probability/Moments/SubGaussian.lean

Modified Mathlib/Probability/Moments/Variance.lean

Modified Mathlib/Probability/Process/Adapted.lean

Modified Mathlib/Probability/Process/Stopping.lean

Modified Mathlib/Probability/StrongLaw.lean

Modified Mathlib/RepresentationTheory/FiniteIndex.lean

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified Mathlib/RingTheory/Congruence/BigOperators.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

added theorem Ideal.map_algebraMap_eq_finsetProd_pow

deleted theorem Ideal.map_algebraMap_eq_finset_prod_pow

Modified Mathlib/RingTheory/Flat/EquationalCriterion.lean

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean

Modified Mathlib/RingTheory/GradedAlgebra/Homogeneous/Subsemiring.lean

Modified Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean

Modified Mathlib/RingTheory/Ideal/Norm/RelNorm.lean

Modified Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean

Modified Mathlib/RingTheory/Invariant/Basic.lean

Modified Mathlib/RingTheory/Kaehler/Basic.lean

Modified Mathlib/RingTheory/Localization/Integer.lean

Modified Mathlib/RingTheory/Localization/Integral.lean

Modified Mathlib/RingTheory/Morita/Matrix.lean

Modified Mathlib/RingTheory/MvPolynomial/Basic.lean

Modified Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean

Modified Mathlib/RingTheory/MvPowerSeries/PiTopology.lean

Modified Mathlib/RingTheory/Polynomial/Basic.lean

Modified Mathlib/RingTheory/Polynomial/Cyclotomic/Eval.lean

Modified Mathlib/RingTheory/Polynomial/Eisenstein/IsIntegral.lean

Modified Mathlib/RingTheory/Polynomial/HilbertPoly.lean

Modified Mathlib/RingTheory/Polynomial/Ideal.lean

Modified Mathlib/RingTheory/Polynomial/ShiftedLegendre.lean

Modified Mathlib/RingTheory/Polynomial/Subring.lean

Modified Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

Modified Mathlib/RingTheory/Polynomial/Vieta.lean

Modified Mathlib/RingTheory/PolynomialAlgebra.lean

Modified Mathlib/RingTheory/PowerSeries/Basic.lean

Modified Mathlib/RingTheory/PowerSeries/Restricted.lean

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Basic.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

Modified Mathlib/Topology/Algebra/InfiniteSum/ENNReal.lean

Modified Mathlib/Topology/Algebra/Module/Basic.lean

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem ContinuousLinearMap.comp_finsetSum

deleted theorem ContinuousLinearMap.comp_finset_sum

added theorem ContinuousLinearMap.finsetSum_comp

deleted theorem ContinuousLinearMap.finset_sum_comp

Modified Mathlib/Topology/Algebra/Module/Multilinear/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

added theorem continuousOn_finsetProd

deleted theorem continuousOn_finset_prod

added theorem continuous_finsetProd

deleted theorem continuous_finset_prod

added theorem tendsto_finsetProd

deleted theorem tendsto_finset_prod

Modified Mathlib/Topology/Algebra/Monoid/FunOnFinite.lean

Modified Mathlib/Topology/Algebra/Polynomial.lean

Modified Mathlib/Topology/Algebra/Ring/Compact.lean

Modified Mathlib/Topology/EMetricSpace/BoundedVariation.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

added theorem ENNReal.tendsto_finsetProd_of_ne_top

deleted theorem ENNReal.tendsto_finset_prod_of_ne_top

Modified Mathlib/Topology/Instances/Matrix.lean

Modified scripts/nolints_prime_decls.txt