Commit 2023-12-04 11:39 aca3f237

View on Github →

chore: remove deprecated MonoidHom.map_prod, AddMonoidHom.map_sum (#8787)

Estimated changes

Modified Mathlib/Algebra/BigOperators/Basic.lean

Modified Mathlib/Algebra/BigOperators/Finprod.lean

Modified Mathlib/Algebra/BigOperators/Finsupp.lean

Modified Mathlib/Algebra/BigOperators/Order.lean

deleted theorem AbsoluteValue.map_prod

Modified Mathlib/Algebra/BigOperators/Pi.lean

Modified Mathlib/Algebra/IndicatorFunction.lean

Modified Mathlib/Algebra/Module/BigOperators.lean

Modified Mathlib/Analysis/BoxIntegral/Partition/Additive.lean

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

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

Modified Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Modified Mathlib/CategoryTheory/Preadditive/AdditiveFunctor.lean

deleted theorem CategoryTheory.Functor.map_sum

Modified Mathlib/CategoryTheory/Preadditive/Opposite.lean

Modified Mathlib/Data/Complex/BigOperators.lean

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/Data/Finsupp/Basic.lean

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/Data/MvPolynomial/Basic.lean

Modified Mathlib/Data/Polynomial/Eval.lean

Modified Mathlib/Data/Real/ENNReal.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

Modified Mathlib/GroupTheory/GroupAction/BigOperators.lean

Modified Mathlib/GroupTheory/Submonoid/Membership.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/MeasureTheory/Measure/MeasureSpace.lean

Modified Mathlib/NumberTheory/Wilson.lean

Modified Mathlib/Probability/Kernel/Basic.lean

Modified Mathlib/RingTheory/Localization/Basic.lean

Modified Mathlib/RingTheory/Localization/Integer.lean

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

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

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

Modified Mathlib/Topology/ContinuousFunction/Algebra.lean

Modified Mathlib/Topology/ContinuousFunction/Bounded.lean