Commit 2023-10-02 15:09 89ef3110

View on Github →

chore: drop redundant LinearMap/LinearEquiv.map_sum (#7426) Note that _root_.map_sum is not marked as @[simp].

Estimated changes

Modified Mathlib/LinearAlgebra/Alternating/Basic.lean

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearEquiv.map_sum

deleted theorem LinearMap.map_sum

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/LinearAlgebra/Matrix/Adjugate.lean

Modified Mathlib/LinearAlgebra/Pi.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean