Commit 2023-09-22 11:29 5f0e89dd

View on Github →

chore: drop redundant LinearMap/LinearEquiv.map_finsupp_sum (#7313)

Estimated changes

Modified Mathlib/Algebra/Module/Projective.lean

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearEquiv.map_finsupp_sum

deleted theorem LinearMap.map_finsupp_sum

Modified Mathlib/LinearAlgebra/FreeModule/PID.lean