Commit 2024-04-29 09:44 ae4dd74c

View on Github →

chore: remove redundant LinearEquiv.map_neg/sub (#12330) These are redundant with _root_.{map_neg,map_sub}.

Estimated changes

Modified Mathlib/Algebra/Lie/Matrix.lean

Modified Mathlib/Algebra/Lie/OfAssociative.lean

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

Modified Mathlib/LinearAlgebra/Basic.lean

deleted theorem LinearEquiv.map_neg

deleted theorem LinearEquiv.map_sub

Modified Mathlib/LinearAlgebra/Basis.lean

Modified Mathlib/NumberTheory/ClassNumber/Finite.lean