Commit 2023-09-14 13:42 9749c637

View on Github →

chore: unify map_dfinsupp_sum/prod lemmas (#7151)

Estimated changes

Modified Mathlib/Data/DFinsupp/Basic.lean

deleted theorem MonoidHom.map_dfinsupp_prod

deleted theorem MulEquiv.map_dfinsupp_prod

deleted theorem RingHom.map_dfinsupp_prod

deleted theorem RingHom.map_dfinsupp_sum

added theorem map_dfinsupp_prod

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearEquiv.map_dfinsupp_sum

deleted theorem LinearMap.map_dfinsupp_sum

Modified Mathlib/LinearAlgebra/Eigenspace/Basic.lean