Commit 2023-09-16 12:55 1fa13fb0

View on Github →

chore: use _root_.map_sum more consistently (#7189) Also _root_.map_smul when in the neighbourhood.

Estimated changes

Modified Mathlib/Algebra/DirectLimit.lean

Modified Mathlib/Algebra/Module/Zlattice.lean

Modified Mathlib/Algebra/TrivSqZeroExt.lean

Modified Mathlib/Analysis/InnerProductSpace/Basic.lean

Modified Mathlib/Analysis/InnerProductSpace/Spectrum.lean

Modified Mathlib/Data/Matrix/Kronecker.lean

Modified Mathlib/Data/Matrix/Rank.lean

Modified Mathlib/Data/Polynomial/AlgebraMap.lean

Modified Mathlib/Data/Polynomial/Coeff.lean

Modified Mathlib/Data/Polynomial/Derivative.lean

Modified Mathlib/Data/Polynomial/HasseDeriv.lean

Modified Mathlib/Data/Polynomial/Taylor.lean

Modified Mathlib/FieldTheory/Finite/Polynomial.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Combination.lean

Modified Mathlib/LinearAlgebra/Alternating.lean

Modified Mathlib/LinearAlgebra/Basic.lean

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/BilinearForm.lean

Modified Mathlib/LinearAlgebra/BilinearMap.lean

Modified Mathlib/LinearAlgebra/Coevaluation.lean

Modified Mathlib/LinearAlgebra/Contraction.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/Finsupp.lean

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean

Modified Mathlib/LinearAlgebra/LinearIndependent.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

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

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean

Modified Mathlib/NumberTheory/RamificationInertia.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Basic.lean

Modified Mathlib/RingTheory/Adjoin/PowerBasis.lean

Modified Mathlib/RingTheory/Derivation/Basic.lean

deleted theorem Derivation.map_sum

Modified Mathlib/RingTheory/Discriminant.lean

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/Ideal/Quotient.lean

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

Modified Mathlib/RingTheory/PowerBasis.lean

Modified Mathlib/RingTheory/PowerSeries/WellKnown.lean

Modified Mathlib/RingTheory/Trace.lean

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