Commit 2024-02-15 11:58 d43978d8

View on Github →

feat: add lemma LinearMap.trace_lie and move Bracket instance (#10584) It is useful to have access to this bracket definition without having to import a bunch of Lie algebra theory.

Estimated changes

Modified Mathlib/Algebra/Lie/OfAssociative.lean

deleted theorem Commute.lie_eq

deleted theorem Ring.lie_def

deleted theorem commute_iff_lie_eq

Modified Mathlib/Algebra/Ring/Commute.lean

added theorem Commute.lie_eq

added theorem Ring.lie_def

added theorem commute_iff_lie_eq

Modified Mathlib/LinearAlgebra/Trace.lean

added theorem LinearMap.trace_lie

Modified test/NoncommRing.lean