Commit 2025-07-15 08:10 d660e92a

View on Github →

chore: golf LinearAlgebra/ using grind (#26685)

Estimated changes

Modified Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Independent.lean

Modified Mathlib/LinearAlgebra/Dimension/DivisionRing.lean

Modified Mathlib/LinearAlgebra/LinearPMap.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

Modified Mathlib/LinearAlgebra/Multilinear/Basic.lean

Modified Mathlib/LinearAlgebra/RootSystem/Basic.lean