Commit 2025-05-06 11:37 8f670641

View on Github →

refactor: make LieAlgebra.SpecialLinear.Eb take an r argument (#24613) This makes it more consistent with Matrix.stdBasisMatrix. Also flips some Ne arguments to match the argument order.

Estimated changes

Modified Mathlib/Algebra/Lie/Classical.lean

modified def LieAlgebra.SpecialLinear.Eb

modified theorem LieAlgebra.SpecialLinear.eb_val

Modified Mathlib/Data/Matrix/Basis.lean

modified theorem Matrix.StdBasisMatrix.diag_zero

Modified Mathlib/LinearAlgebra/Matrix/Trace.lean

modified theorem Matrix.StdBasisMatrix.trace_zero

Modified Mathlib/LinearAlgebra/Trace.lean