Commit 2025-02-15 09:40 fc1556c1

View on Github →

chore(LinearAlgebra): fix some Fintype/DecidableEq (#21898) Found by the linters in #10235

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/BaseChange.lean

Modified Mathlib/LinearAlgebra/Matrix/Basis.lean

modified theorem Basis.toMatrix_mulVec_repr

Modified Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean